{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T18:37:48Z","timestamp":1767638268983,"version":"3.48.0"},"reference-count":36,"publisher":"Maximum Academic Press","issue":"3","license":[{"start":{"date-parts":[[2012,7,26]],"date-time":"2012-07-26T00:00:00Z","timestamp":1343260800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Knowledge Engineering Review"],"published-print":{"date-parts":[[2012,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Safety-critical software must be thoroughly verified before being exploited in commercial applications. In particular, any TCAS (Traffic Alert and Collision Avoidance System) implementation must be verified against safety properties extracted from the anti-collision theory that regulates the controlled airspace. This verification step is currently realized with manual code reviews and testing. In our work, we explore the capabilities of Constraint Programming for automated software verification and testing. We built a dedicated constraint solving procedure that combines constraint propagation with Linear Programming to solve conditional disjunctive constraint systems over bounded integers extracted from computer programs and safety properties. An experience we made on verifying a publicly available TCAS component implementation against a set of safety-critical properties showed that this approach is viable and efficient.<\/jats:p>","DOI":"10.1017\/s0269888912000252","type":"journal-article","created":{"date-parts":[[2012,7,26]],"date-time":"2012-07-26T05:43:52Z","timestamp":1343281432000},"page":"343-360","source":"Crossref","is-referenced-by-count":22,"title":["TCAS software verification using constraint programming"],"prefix":"10.48130","volume":"27","author":[{"given":"Arnaud","family":"Gotlieb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"27968","published-online":{"date-parts":[[2012,7,26]]},"reference":[{"key":"S0269888912000252_ref36","doi-asserted-by":"crossref","unstructured":"Williams N. , Marre B. , Mouy P. , Roger M. 2005. PathCrawler: automatic generation of path tests by combining static and dynamic analysis. In Proceedings of Dependable Computing\u2014EDCC'05, 281\u2013292. Budapest, Hungary.","DOI":"10.1007\/11408901_21"},{"key":"S0269888912000252_ref33","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S. , Col\u00f2n M. A. , Sipma H. , Manna Z. 2006. Efficient strongly relational polyhedral analysis. In Proceedings of VMCAI'06, 115\u2013125. Charleston, SC, USA.","DOI":"10.1007\/11609773_8"},{"key":"S0269888912000252_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0433-3"},{"key":"S0269888912000252_ref28","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.14.4.387.2830"},{"key":"S0269888912000252_ref9","unstructured":"Holzbaur C. 1995. OFAI clp(q,r) Manual, 1.3.3 edition. Austrian Research Institute for Artificial Intelligence."},{"key":"S0269888912000252_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900001077"},{"key":"S0269888912000252_ref23","doi-asserted-by":"crossref","unstructured":"Henzinger T. , Jhala R. , Majumdar R. , Sutre G. 2003. Software verification with blast. In Proceedings of the 10th Workshop on Model Checking of Software (SPIN), 235\u2013239. Portland, OR, USA.","DOI":"10.1007\/3-540-44829-2_17"},{"key":"S0269888912000252_ref18","doi-asserted-by":"crossref","unstructured":"Godefroid P. , Klarlund N. , Sen K. 2005. Dart: directed automated random testing. In Proceedings of the PLDI'05, 213\u2013223. Chicago, IL, USA.","DOI":"10.1145\/1065010.1065036"},{"key":"S0269888912000252_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-005-3861-2"},{"key":"S0269888912000252_ref14","doi-asserted-by":"crossref","unstructured":"Denmat T. , Gotlieb A. , Ducasse M. 2007a. An abstract interpretation based combinator for modeling while loops in constraint programming. In Proceedings of Principles and Practices of Constraint Programming (CP'07), Lecture Notes in Computer Science, 4741, 241\u2013255. Springer Verlag.","DOI":"10.1007\/978-3-540-74970-7_19"},{"key":"S0269888912000252_ref13","doi-asserted-by":"publisher","DOI":"10.1109\/32.92910"},{"key":"S0269888912000252_ref10","unstructured":"Coen-Porisini A. , Denaro G. , Ghezzi C. , Pezze M. 2001. Using symbolic execution for verifying safety-critical systems. In Proceedings of the European Software Engineering Conference (ESEC\/FSE'01), ACM, 142\u2013150."},{"key":"S0269888912000252_ref5","doi-asserted-by":"crossref","unstructured":"Brummayer R. , Biere A. 2007. C32SAT: checking C expressions. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science, 4590, 294\u2013297. Springer.","DOI":"10.1007\/978-3-540-73368-3_33"},{"key":"S0269888912000252_ref3","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.333"},{"key":"S0269888912000252_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.226498"},{"key":"S0269888912000252_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-004-5307-7"},{"key":"S0269888912000252_ref35","unstructured":"U.S. Department of Transportation Federal Aviation Administration 2000. Introduction to TCAS II \u2014version 7."},{"key":"S0269888912000252_ref17","unstructured":"DO-178B\/ED-12B. 1992. Software Considerations in Airborn Systems and Equipment Certification, RTCA and EUROCAE. Inc Washington, DC, USA and EUROCAE, Paris, France."},{"key":"S0269888912000252_ref22","unstructured":"Rossi F. , van Beek P. , Walsh T. (eds). 2006. Handbook of Constraint Programming. Elsevier."},{"key":"S0269888912000252_ref26","doi-asserted-by":"crossref","unstructured":"Livadas C. , Lygeros J. , Lynch N. A. 1999. High-level modeling and analysis of TCAS. In IEEE Real-Time Systems Symposium, 115\u2013125. Phoenix, AZ, USA.","DOI":"10.1109\/REAL.1999.818833"},{"key":"S0269888912000252_ref30","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199902)29:2<167::AID-SPE225>3.0.CO;2-V"},{"key":"S0269888912000252_ref15","doi-asserted-by":"crossref","unstructured":"Denmat T. , Gotlieb A. , Ducasse M. 2007b. Improving constraint-based testing with dynamic linear relaxations. In Proceedings of the 18th IEEE International Symposium on Software Reliability Engineering (ISSRE\u2019 2007), Trollh\u00e4ttan, Sweden.","DOI":"10.1109\/ISSRE.2007.34"},{"key":"S0269888912000252_ref8","doi-asserted-by":"crossref","unstructured":"Clarke E. , Kroening D. 2003. Hardware verification using ANSI-C programs as a reference. In Proceedings of the ASP-DAC'03, 308\u2013311. Kitakyushu, Japan.","DOI":"10.1145\/1119772.1119831"},{"key":"S0269888912000252_ref19","unstructured":"Gotlieb A. , Botella B. , Rueher M. 2000. A CLP framework for computing structural test data. In Proceedings of Computational Logic (CL'2000), London, UK, Lecture Notes in Artificial Intelligence, 1891, 399\u2013413."},{"key":"S0269888912000252_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2006.10.016"},{"key":"S0269888912000252_ref11","doi-asserted-by":"crossref","unstructured":"Collavizza H. , Rueher M. 2006. Exploration of the capabilities of constraint programming for software verification. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), 182\u2013196. Springer, Vienna, Austria.","DOI":"10.1007\/11691372_12"},{"key":"S0269888912000252_ref21","doi-asserted-by":"crossref","unstructured":"Gotlieb A. 2009. Euclide: a constraint-based testing platform for critical C programs. In 2nd International Conference on Software Testing, Validation and Verification (ICST'09), Denver, CO.","DOI":"10.1109\/ICST.2009.10"},{"key":"S0269888912000252_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197331"},{"key":"S0269888912000252_ref34","unstructured":"Sen K. , Marinov D. , Agha G. 2005. CUTE: a concolic unit testing engine for C. In Proceedings of ESEC\/FSE-13, ACM Press, 263\u2013272."},{"key":"S0269888912000252_ref12","doi-asserted-by":"crossref","unstructured":"Collavizza H. , Rueher M. , Van Hentenryck P. 2008. CPBPV: a constraint-programming framework for bounded program verification. In Proceedings of CP2008, Lecture Notes in Computer Science, 5202, 327\u2013341. Springer.","DOI":"10.1007\/978-3-540-85958-1_22"},{"key":"S0269888912000252_ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"S0269888912000252_ref31","doi-asserted-by":"crossref","unstructured":"Randimbivololona F. 2001. Orientations in Verification Engineering of Avionics Software. In Informatics, 10 Years Back, 10 Years Ahead, Reinhard Wilhelm. Lecture Notes in Computer Science 2000, 131\u2013137. Springer.","DOI":"10.1007\/3-540-44577-3_9"},{"key":"S0269888912000252_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/BF01580665"},{"key":"S0269888912000252_ref6","doi-asserted-by":"crossref","unstructured":"Carlsson M. , Ottosson G. , Carlson B. 1997. An open-ended finite domain constraint solver. In Proceedings of the Programming Languages: Implementations, Logics, and Programs. Lecturer Notes in Computer Science, 1292, 191\u2013206. Springer, Southampton, UK.","DOI":"10.1007\/BFb0033845"},{"key":"S0269888912000252_ref32","doi-asserted-by":"crossref","unstructured":"Refalo P. 1999. Tight cooperation and its application in piecewise linear optimization. In Proceedings of CP'99, Alexandria, Virginia.","DOI":"10.1007\/978-3-540-48085-3_27"},{"key":"S0269888912000252_ref1","doi-asserted-by":"publisher","DOI":"10.1137\/0606047"}],"container-title":["The Knowledge Engineering Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0269888912000252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T14:44:07Z","timestamp":1767624247000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0269888912000252\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,26]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,7,26]]}},"alternative-id":["S0269888912000252"],"URL":"https:\/\/doi.org\/10.1017\/s0269888912000252","relation":{},"ISSN":["0269-8889","1469-8005"],"issn-type":[{"type":"print","value":"0269-8889"},{"type":"electronic","value":"1469-8005"}],"subject":[],"published":{"date-parts":[[2012,7,26]]}}}