Modular verification of software components in C

By Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith. 25th International Conference on Software Engineering, 2003. Proceedings., 2003

554 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/1265bce617702450d13e0e0d11c0cc36d57fb841

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Rupak Majumdar
2. Sriram K. Rajamani
3. Thomas Ball
4. Ranjit Jhala
5. Kenneth L. McMillan
6. Andreas Podelski
7. Hongseok Yang
8. Byron Cook

In Computational Theory and Mathematics

1. Kenneth L. McMillan
2. Ranjit Jhala
3. Rupak Majumdar
4. Dirk Beyer
5. Andreas Podelski
6. Shaz Qadeer
7. Daniel Kroening
8. Hongseok Yang

In Software

1. Kenneth L. McMillan
2. Rupak Majumdar
3. Ranjit Jhala
4. Dirk Beyer
5. Hongseok Yang
6. Shaz Qadeer
7. Sriram K. Rajamani
8. Thomas Ball

Citations in the corpus

• SATABS: SAT-Based Predicate Abstraction for ANSI-C (2005, methodology): “Thus, there are already a number of other implementations, such as Magic [8], ComFoRT [9] and Blast [10].”
• Transition invariants (2004, methodology): “Such methods have helped to realize the potential of the inductive proof rules for (state) invariants [14] for the automation of the verification of safety properties [1, 2, 3, 4, 5, 7, 8].”
• Context-Bounded Model Checking of Concurrent Software (2005, methodology): “A variety of automated compositional techniques for verifying concurrent software have been developed [6, 16, 13, 15].”
• The software model checker Blast (2007, methodology): “Implementations of CEGAR include Slam, Blast, Magic, Moped, SatAbs, and F- Soft [4,17,23,33,54].”
• A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “In the next section, we discuss methods for reasoning about formulas arising in BMC.”
• Thorough static analysis of device drivers (2006, methodology): “In addition to Slam , other tools have been built to check safety properties of C programs using iterative refinement, notably Blast [35] and Magic [13].”
• ACSAR: Software Model Checking with Transfinite Refinement (2007, methodology): “ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement ) is a software model checker for C programs in the spirit of Blast [5], F-Soft [6], Magic [4] and Slam [1].”
• Learning a strategy for adapting a program analysis via bayesian optimisation (2015, methodology): “Such analyses commonly adopt counter-example-guided abstraction refinement, and selects a program abstraction based on the feedback from a failed analysis run [1, 4–6, 8, 9, 31, 32].”
• Lazy Abstraction with Interpolants (2006, methodology): “This is implemented using the lazy paradigm in the Blast model checker [7], and in a number of software model checkers [2,4,3] using a counterexamplebased refinement loop.”
• Perracotta: mining temporal API rules from imperfect traces (2006, background): “This section provides background on temporal properties and program verification, and discusses related work in static and dynamic property inference.”