Context-Bounded model checking with ESBMC 1.17
作者： Lucas Cordeiro , Jeremy Morse , Denis Nicole , Bernd Fischer
DOI: 10.1007/978-3-642-28756-5_42
关键词:
摘要: ESBMC is a context-bounded symbolic model checker for single- and multi-threaded ANSI-C code. It converts the verification conditions using different background theories passes them directly to an SMT solver.
springer.com
core.ac.uk
sci-hub.st 参考文章(7)
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer, Context-bounded model checking of LTL properties for ANSI-C software international conference on software engineering. pp. 302- 317 ,(2011) , 10.1007/978-3-642-24690-6_21
Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva, SMT-Based Bounded Model Checking for Embedded ANSI-C Software automated software engineering. ,vol. 38, pp. 957- 974 ,(2009) , 10.1109/ASE.2009.63
Lucas Cordeiro, Bernd Fischer, Verifying multi-threaded software using smt-based context-bounded model checking international conference on software engineering. pp. 331- 340 ,(2011) , 10.1145/1985793.1985839
Edmund Clarke, Daniel Kroening, Flavio Lerda, A Tool for Checking ANSI-C Programs tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 168- 176 ,(2004) , 10.1007/978-3-540-24730-2_15
Lucas Cordeiro, SMT-based bounded model checking for multi-threaded software in embedded systems international conference on software engineering. ,vol. 2, pp. 373- 376 ,(2010) , 10.1145/1810295.1810396
Alessandro Cimatti, Marco Roveri, Iman Narasamdya, Andrea Micheli, Verifying SystemC: a software model checking approach formal methods in computer-aided design. pp. 51- 60 ,(2010) , 10.5555/1998496.1998510