Using DimSpec for Bounded and Unbounded Software Model Checking
| Autor: | Carsten Sinz, Marko Kleine Büning, Tomáš Balyo |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Model checking
050101 languages & linguistics Exploit Computer science Programming language 05 social sciences 02 engineering and technology Solver computer.software_genre Propositional calculus Software model checking Bounded function 0202 electrical engineering electronic engineering information engineering Benchmark (computing) 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences computer Software verification |
| Zdroj: | Formal Methods and Software Engineering ISBN: 9783030324087 ICFEM |
| Popis: | This paper describes a unified approach for both bounded and unbounded software model checking to find errors in programs written in the programming language C. It is based on a propositional logic intermediate representation, called DimSpec, that has been successfully applied in SAT-based automated planning. Using DimSpec formulas allows us to exploit the advantages of incremental SAT solving and provides an alternative approach to using the universal incremental SAT API IPASIR or native solver APIs. The DimSpec formula can be used for bounded model checking (via incremental SAT solving) as well as unbounded model checking (using a backend that implements an IC3-style algorithm). We also present an implementation of our approach, called LLUMC, which encodes the presence of certain errors in a C program into a DimSpec formula. We evaluate our approach on benchmark problems from the Software Verification Competition (SV-COMP) and compare it with other tools to demonstrate runtime and functionality advantages compared to state-of-the-art solvers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|