KRATOS swMATH ID: 7808 Software Authors: A. Cimatti, A. Griggio, A. Micheli, I. Narasamdya, M. Roveri Description: KRATOS: A software model checker for SystemC. he growing popularity of SystemC has attracted research aimed at the formal verification of SystemC designs. In this paper we present Kratos, a software model checker for SystemC. Kratos verifies safety properties, in the form of program assertions, by allowing users to explore two directions in the verification. First, by relying on the translation from SystemC designs to sequential C programs, Kratos is capable of model checking the resulting C programs using the symbolic lazy predicate abstraction technique. Second, Kratos implements a novel algorithm, called ESST, that combines Explicit state techniques to deal with the SystemC Scheduler, with Symbolic techniques to deal with the Threads. Kratos is built on top of NuSMV and MathSat, and uses state-of-the-art SMT-based techniques for program abstractions and refinements Homepage: http://rd.springer.com/chapter/10.1007/978-3-642-22110-1_24 Related Software: BLAST; SystemC; SatAbs; LusSy; veriSoft; Wolverine; DDVerify; SLAM; Circus; ProofPower; z3; TPTP; SMT-LIB; VAMPIRE; LLVM; SPIN; Interproc; YOGI; TRACER; CPAchecker Cited in: 7 Publications all top 5 Cited by 19 Authors 2 Cimatti, Alessandro 2 Narasamdya, Iman 2 Roveri, Marco 1 Brooke, Phillip J. 1 Dams, Dennis René 1 Ebnenasir, Ali 1 Grumberg, Orna 1 Hajisheykhi, Reza 1 He, Jifeng 1 Hoder, Kryštof 1 Jaffar, Joxan 1 Kovács, Laura Ildikó 1 Kulkarni, Sandeep S. 1 Murali, Vijayaraghavan 1 Navas, Jorge A. 1 Qin, Shengchao 1 Santosa, Andrew E. 1 Voronkov, Andrei 1 Zhu, Huibiao Cited in 3 Serials 1 Theoretical Computer Science 1 Formal Aspects of Computing 1 Logical Methods in Computer Science Cited in 1 Field 7 Computer science (68-XX) Citations by Year