{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:11:03Z","timestamp":1767928263301,"version":"3.49.0"},"reference-count":59,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,26]],"date-time":"2012-03-26T00:00:00Z","timestamp":1332720000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a static analysis by Abstract Interpretation to check for run-time errors in parallel and multi-threaded C programs. Following our work on Astr\\'ee, we focus on embedded critical programs without recursion nor dynamic memory allocation, but extend the analysis to a static set of threads communicating implicitly through a shared memory and explicitly using a finite set of mutual exclusion locks, and scheduled according to a real-time scheduling policy and fixed priorities. Our method is thread-modular. It is based on a slightly modified non-parallel analysis that, when analyzing a thread, applies and enriches an abstract set of thread interferences. An iterator then re-analyzes each thread in turn until interferences stabilize. We prove the soundness of our method with respect to the sequential consistency semantics, but also with respect to a reasonable weakly consistent memory semantics. We also show how to take into account mutual exclusion and thread priorities through a partitioning over an abstraction of the scheduler state. We present preliminary experimental results analyzing an industrial program with our prototype, Th\\'es\\'ee, and demonstrate the scalability of our approach.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:26)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":26,"title":["Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Antoine","family":"Min\u00e9","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,26]]},"reference":[{"key":"10.2168\/LMCS-8(1:26)2012_absint-web","unstructured":"AbsInt, Angewandte Informatik. Astr\u00e9e run-time error analyzer. http:\/\/www.absint.com\/astree."},{"key":"10.2168\/LMCS-8(1:26)2012_adve-charachorloo-WRL95","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"10.2168\/LMCS-8(1:26)2012_ARINC","unstructured":"Aeronautical Radio Inc. ARINC 653. http:\/\/www.arinc.com."},{"key":"10.2168\/LMCS-8(1:26)2012_algave-aplas11","doi-asserted-by":"crossref","unstructured":"J. Alglave, D. Kroening, J. Lugton, V. Nimal, and M. Tautschnig. Soundness of data flow analyses for weak memory models. InProc. of the 9th Asian Symp. on Programming Languages and Systems (APLAS'2011), volume 7078 ofLNCS, pages 272-288, Dec. 2011.","DOI":"10.1007\/978-3-642-25318-8_21"},{"key":"10.2168\/LMCS-8(1:26)2012_alglave-al-tacas11","doi-asserted-by":"crossref","unstructured":"J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Litmus: Running tests against hardware. InProc. of 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 ofLNCS, pages 41-44. Springer, Mar. 2011.","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"10.2168\/LMCS-8(1:26)2012_atig-al-popl10","doi-asserted-by":"crossref","unstructured":"M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. On the verification problem for weak memory models. InProc. of the 37th ACM SIGACT\/SIGPLAN Symp. on Principles of Programming Languages (POPL'10), pages 7-18. ACM, Jan. 2010.","DOI":"10.1145\/1706299.1706303"},{"key":"10.2168\/LMCS-8(1:26)2012_bertrane-al-aiaa10","doi-asserted-by":"crossref","unstructured":"J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, and X. Rival. Static analysis and verification of aerospace software by abstract interpretation. InAIAA Infotech@Aerospace, number 2010-3385 in AIAA, pages 1-38. AIAA (American Institute of Aeronautics and Astronautics), Apr. 2010.","DOI":"10.2514\/6.2010-3385"},{"key":"10.2168\/LMCS-8(1:26)2012_blanchet-al-PLDI03","doi-asserted-by":"crossref","unstructured":"B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. InProc. of the ACM SIGPLAN Conf. on Programming Languages Design and Implementation (PLDI'03), pages 196-207. ACM, June 2003.","DOI":"10.1145\/781131.781153"},{"key":"10.2168\/LMCS-8(1:26)2012_mine:dasia09","unstructured":"O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, K. Ghorbal, E. Goubault, D. Lesens, L. Mauborgne, A. Min\u00e9, S. Putot, X. Rival, and M. Turin. Space software validation using abstract interpretation. InProc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DASIA'09), volume SP-669, pages 1-7. ESA, May 2009."},{"key":"10.2168\/LMCS-8(1:26)2012_bourdoncle-FMPA93","doi-asserted-by":"crossref","unstructured":"F. Bourdoncle. Efficient chaotic iteration strategies with widenings. InProc. of the Int. Conf. on Formal Methods in Programming and their Applications (FMPA'93), volume 735 ofLNCS, pages 128-141. Springer, June 1993.","DOI":"10.1007\/BFb0039704"},{"key":"10.2168\/LMCS-8(1:26)2012_carre-hymans-ARXIV09","unstructured":"J.-L. Carr\u00e9 and C. Hymans. From single-thread to multithreaded: An efficient static analysis algorithm. Technical Report arXiv:0910.5833v1, EADS, Oct. 2009."},{"key":"10.2168\/LMCS-8(1:26)2012_chang-al:popl08","doi-asserted-by":"crossref","unstructured":"B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. InProc. of the 35th ACM SIGPLAN\/SIGACT Symp. on Principles of Programming Languages (POPL'08), pages 247-260. ACM, 2008.","DOI":"10.1145\/1328438.1328469"},{"key":"10.2168\/LMCS-8(1:26)2012_cc-POPL77","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProc. of the 4th ACM Symp. on Principles of Programming Languages (POPL'77), pages 238-252. ACM, Jan. 1977.","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"10.2168\/LMCS-8(1:26)2012_cc-PJM79","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"81","author":"P. Cousot and R. Cousot","year":"1979","journal-title":"Pacific Journal of Mathematics"},{"key":"10.2168\/LMCS-8(1:26)2012_cc-APCT84","unstructured":"P. Cousot and R. Cousot. Invariance proof methods and analysis techniques for parallel programs. InAutomatic Program Construction Techniques, chapter 12, pages 243-271. Macmillan, New York, NY, USA, 1984."},{"key":"10.2168\/LMCS-8(1:26)2012_cc-JLC92","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"10.2168\/LMCS-8(1:26)2012_cc-PLILP92","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation, invited paper. InInt. Workshop on Programming Language Implementation and Logic Programming (PLILP'92), volume 631 ofLNCS, pages 269-295. Springer, 1992.","DOI":"10.1007\/3-540-55844-6_142"},{"key":"10.2168\/LMCS-8(1:26)2012_cousot-al-ASIAN06","doi-asserted-by":"crossref","unstructured":"P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. Combination of abstractions in the Astr\u00e9e static analyzer. InProc. of the 11th Annual Asian Computing Science Conf. (ASIAN'06), volume 4435 ofLNCS, pages 272-300. Springer, Dec. 2006.","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"10.2168\/LMCS-8(1:26)2012_mine-al:tase07","doi-asserted-by":"crossref","unstructured":"P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. Varieties of static analyzers: A comparison with Astr\u00e9e, invited paper. InProc. of the First IEEE & IFIP Int. Symp. on Theoretical Aspects of Software Engineering (TASE'07), pages 3-17. IEEE CS Press, June 2007.","DOI":"10.1109\/TASE.2007.55"},{"key":"10.2168\/LMCS-8(1:26)2012_astreea-web","unstructured":"P. Cousot, R. Cousot, J. Feret, A. Min\u00e9, and X. Rival. The Astr\u00e9e A static analyzer. http:\/\/www.astreea.ens.fr."},{"key":"10.2168\/LMCS-8(1:26)2012_ch:popl78","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. InConf. Rec. of the 5th Annual ACM SIGPLAN\/SIGACT Symp. on Principles of Programming Languages (POPL'78), pages 84-97. ACM, 1978.","DOI":"10.1145\/512760.512770"},{"key":"10.2168\/LMCS-8(1:26)2012_roever-01","unstructured":"W.-P. de Roever, F. de Boer, U. Hanneman, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers.Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, 2001."},{"key":"10.2168\/LMCS-8(1:26)2012_delmas-souyris-sas07","doi-asserted-by":"crossref","unstructured":"D. Delmas and J. Souyris. Astr\u00e9e: from research to industry. InProc. of the 14th Int. Static Analysis Symp. (SAS'07), volume 4634 ofLNCS, pages 437-451. Springer, Aug. 2007.","DOI":"10.1007\/978-3-540-74061-2_27"},{"key":"10.2168\/LMCS-8(1:26)2012_dijkstra-EWD123","doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. Cooperating sequential processes. InProgramming Languages: NATO Advanced Study Institute, pages 43-112. Academic Press, 1968.","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"10.2168\/LMCS-8(1:26)2012_dijkstra-EWD472","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"10.2168\/LMCS-8(1:26)2012_feret:getcol00","doi-asserted-by":"crossref","unstructured":"J. Feret. Occurrence counting analysis for the pi-calculus.Electronic Notes in Theoretical Computer Science, 39(2), 2001.","DOI":"10.1016\/S1571-0661(05)01155-2"},{"key":"10.2168\/LMCS-8(1:26)2012_feret-ESOP04","doi-asserted-by":"crossref","unstructured":"J. Feret. Static analysis of digital filters. InProc. of the 13th European Symp. on Programming (ESOP'04), volume 2986 ofLNCS, pages 33-48. Springer, Mar. 2004.","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"10.2168\/LMCS-8(1:26)2012_ferrara-TAP08","doi-asserted-by":"crossref","unstructured":"P. Ferrara. Static analysis via abstract interpretation of the happens-before memory model. InProc. of the 2nd Int. Conf. on Tests and Proofs (TAP'08), volume 4966 ofLNCS, pages 116-133. Springer, 2008.","DOI":"10.1007\/978-3-540-79124-9_9"},{"key":"10.2168\/LMCS-8(1:26)2012_flanagan-al-spin03","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S. Qadeer. Thread-modular model checking. InProc. of the 10th Int. SPIN Workshop on Model Checking of Software (SPIN'03), volume 2648 ofLNCS, pages 213-224. Springer, 2003.","DOI":"10.1007\/3-540-44829-2_14"},{"key":"10.2168\/LMCS-8(1:26)2012_gamatie-RTAS03","doi-asserted-by":"crossref","unstructured":"A. Gamati\u00e9 and T. Gautier. Synchronous modeling of avionics applications using the SIGNAL language. InProc. of the 9th IEEE Real-Time and Embedded Technology and Applications Symp. (RTAS'03), pages 144-151. IEEE Computer Society, 2003.","DOI":"10.1109\/RTTAS.2003.1203046"},{"key":"10.2168\/LMCS-8(1:26)2012_godefroid-phd","unstructured":"P. Godefroid.Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis, University of Liege, Computer Science Department, 1994."},{"key":"10.2168\/LMCS-8(1:26)2012_java3","unstructured":"J. Gosling, B. Joy, G. Steele, and G. Bracha.The Java Language Specification. Addison Wesley, 3rd edition, June 2005."},{"key":"10.2168\/LMCS-8(1:26)2012_ieee754","unstructured":"IEEE Computer Society. Standard for binary floating-point arithmetic. Technical report, ANSI\/IEEE Std. 745-1985, 1985."},{"key":"10.2168\/LMCS-8(1:26)2012_posix-threads","unstructured":"IEEE Computer Society and The Open Group. Portable operating system interface (POSIX) - Application program interface (API) amendment 2: Threads extension (C language). Technical report, ANSI\/IEEE Std. 1003.1c-1995, 1995."},{"key":"10.2168\/LMCS-8(1:26)2012_c99","unstructured":"ISO\/IEC JTC1\/SC22\/WG14 working group. C standard. Technical Report 1124, ISO & IEC, 2007."},{"key":"10.2168\/LMCS-8(1:26)2012_mine:cav09","doi-asserted-by":"crossref","unstructured":"B. Jeannet and A. Min\u00e9. Apron: A library of numerical abstract domains for static analysis. InProc. of the 21th Int. Conf. on Computer Aided Verification (CAV'09), volume 5643 ofLNCS, pages 661-667. Springer, June 2009.","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"10.2168\/LMCS-8(1:26)2012_lamport-TSE77","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"10.2168\/LMCS-8(1:26)2012_lamport-ACM78","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"10.2168\/LMCS-8(1:26)2012_lamport-TC79","doi-asserted-by":"crossref","unstructured":"L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. InIEEE Trans. on Computers, volume 28, pages 690-691. IEEE Comp. Soc., Sep. 1979.","DOI":"10.1109\/TC.1979.1675439"},{"key":"10.2168\/LMCS-8(1:26)2012_lamport-AI80","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289062"},{"key":"10.2168\/LMCS-8(1:26)2012_leroy-POPL06","doi-asserted-by":"crossref","unstructured":"X. Leroy. Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. InProc. of the 33rd ACM SIGPLAN\/SIGACT Symp. on Principles of Programming Languages (POPL'06), pages 42-54. ACM, 2006.","DOI":"10.1145\/1111037.1111042"},{"key":"10.2168\/LMCS-8(1:26)2012_malkis-phd","unstructured":"A. Malkis.Cartesian Abstraction and Verification of Multithreaded Programs. PhD thesis, University of Freiburg, 2010."},{"key":"10.2168\/LMCS-8(1:26)2012_manson-al-POPL05","doi-asserted-by":"crossref","unstructured":"J. Manson, B. Pugh, and S. V. Adve. The Java memory model. InProc. of the 32nd ACM SIGPLAN\/SIGACT Symp. on Principles of Programming Languages (POPL'05), pages 378-391. ACM, Jan. 2005.","DOI":"10.1145\/1040305.1040336"},{"key":"10.2168\/LMCS-8(1:26)2012_mauborgne-rival-ESOP05","doi-asserted-by":"crossref","unstructured":"L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzer. InProc. of the 14th European Symp. on Programming (ESOP'05), volume 3444 ofLNCS, pages 5-20. Springer, Apr. 2005.","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"10.2168\/LMCS-8(1:26)2012_mine-LCTES06","doi-asserted-by":"crossref","unstructured":"A. Min\u00e9. Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. InProc. of the ACM SIGPLAN\/SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES'06), pages 54-63. ACM, June 2006.","DOI":"10.1145\/1134650.1134659"},{"key":"10.2168\/LMCS-8(1:26)2012_mine-HOSC06","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"10.2168\/LMCS-8(1:26)2012_mine:esop11","doi-asserted-by":"crossref","unstructured":"A. Min\u00e9. Static analysis of run-time errors in embedded critical parallel C programs. InProc. of the 20th European Symp. on Programming (ESOP'11), volume 6602 ofLNCS, pages 398-418. Springer, Mar. 2011.","DOI":"10.1007\/978-3-642-19718-5_21"},{"key":"10.2168\/LMCS-8(1:26)2012_nielson-al","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. R. Nielson, and C. Hankin.Principles of Program Analysis. Springer, Oct. 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"10.2168\/LMCS-8(1:26)2012_owicki-gries-AI76","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"10.2168\/LMCS-8(1:26)2012_qadeer-rehof-tacas05","doi-asserted-by":"crossref","unstructured":"S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. InProc. of the 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), volume 3440 ofLNCS, pages 93-107. Springer, 2005.","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"10.2168\/LMCS-8(1:26)2012_reynolds-FSTTCS04","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Toward a grainless semantics for shared-variable concurrency. InProc. of the Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), volume 3328 ofLNCS, pages 35-48. Springer, Dec. 2004.","DOI":"10.1007\/978-3-540-30538-5_4"},{"key":"10.2168\/LMCS-8(1:26)2012_rinard-sas01","doi-asserted-by":"crossref","unstructured":"M. C. Rinard. Analysis of multithreaded programs. InProc. of the 8th Int. Static Analysis Symp. (SAS'01), volume 2126 ofLNCS, pages 1-19. Springer, Jul 2001.","DOI":"10.1007\/3-540-47764-0_1"},{"key":"10.2168\/LMCS-8(1:26)2012_salciano-al-ppopp01","doi-asserted-by":"crossref","unstructured":"A. Salcianu and M. Rinard. Pointer and escape analysis for multithreaded programs. InProc. the 8th ACM SIGPLAN Symp. on Principles and Practices of Parallel Programming (PPoPP'01), pages 12-23. ACM, 2001.","DOI":"10.1145\/379539.379553"},{"key":"10.2168\/LMCS-8(1:26)2012_saraswat-al-PPOPP07","doi-asserted-by":"crossref","unstructured":"V. A. Saraswat, R. Jagadeesan, M. M. Michael, and C. von Praun. A theory of memory models. InProc. of the 12th ACM SIGPLAN Symp. on Principles and Practice of Parallel Programs (PPoPP'07), pages 161-172. ACM, Mar. 2007.","DOI":"10.1145\/1229428.1229469"},{"key":"10.2168\/LMCS-8(1:26)2012_sevcik-popl11","doi-asserted-by":"crossref","unstructured":"J. Sevc\u00edk, V. Vafeiadis, F. Zappa Nardelli, P. Sewell, and S. Jagannathan. Relaxed-memory concurrency and verified compilation. InProc. of the 38th ACM SIGACT\/SIGPLAN Symp. on Principles of Programming Languages (POPL'11), pages 43-54. ACM, Jan. 2011.","DOI":"10.1145\/1926385.1926393"},{"key":"10.2168\/LMCS-8(1:26)2012_sewell-al:jacm10","doi-asserted-by":"crossref","unstructured":"P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, and M. Myreen. x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors.Comm. ACM, 53, 2010.","DOI":"10.1145\/1785414.1785443"},{"key":"10.2168\/LMCS-8(1:26)2012_steensgaard-popl96","doi-asserted-by":"crossref","unstructured":"B. Steensgaard. Points-to analysis in almost linear time. InProc. of the 23rd ACM SIGPLAN\/SIGACT Symp. on Principles of Programming Languages (POPL'96), pages 32-41. ACM, 1996.","DOI":"10.1145\/237721.237727"},{"key":"10.2168\/LMCS-8(1:26)2012_tarski-PJM55","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics"},{"key":"10.2168\/LMCS-8(1:26)2012_ima","doi-asserted-by":"crossref","unstructured":"C. B. Watkins and R. Walter. Transitioning from federated avionics architectures to integrated modular avionics. InProc. of the 26th IEEE\/AIAA Digital Avionics Systems Conf. (DASC'07), volume 2.A.1, pages 1-10. IEEE, Oct. 2007.","DOI":"10.1109\/DASC.2007.4391842"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/799\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/799\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:10:00Z","timestamp":1744067400000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/799"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,26]]},"references-count":59,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:26)2012","relation":{"references":[{"id-type":"doi","id":"10.1007\/978-3-540-31987-0_2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1203.3724","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.3724","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,26]]},"article-number":"799"}}