Model checking programs

By Willem Visser, Klaus Havelund, Guillaume P. Brat, Seungjoon Park, Flavio Lerda. Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, 2000

1,585 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/b6404d98730b9732ebdfd41cb9c8ad18046fd5a1

How researchers see this paper

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

In Computational Theory and Mathematics

In Software

Citations in the corpus

Using model checking to find serious file system errors (2004, methodology): “Java PathFinder [ Brat et al. 2000 ] is very similar to CMC and systematically checks concurrent Java programs by checkpointing states.”
A Classification and Survey of Analysis Strategies for Software Product Lines (2014, methodology): “NUSMV [Cimatti et al. 1999]), while others extract models directly from source code (e.g., C in BLAST [Beyer et al. 2007] or CPACHECKER [Beyer and Keremoglu 2011], Java in JPF[Visser et al. 2000]).”
Software model checking (2009, positive): “JavaPathFinder is an execution-based model checker for Java programs that uses the Java Virtual Machine rather than the OS scheduler, to analyze diﬀerent schedules [Visser et al. 2003; Havelund and Pressburger 2000].”
Race directed random testing of concurrent programs (2008, background): “Static verification [4, 16, 28, 40, 8] and model checking [17, 29, 25, 27, 52, 31] or path-sensitive search of the state space is an alternative approach to finding bugs in concurrent programs.”
Perracotta: mining temporal API rules from imperfect traces (2006, methodology): “Much research has focused on using specifications of temporal properties to verify systems, especially concurrent systems [2, 5, 9, 10, 13, 14, 18, 27, 33, 47].”
Generalized Symbolic Execution for Model Checking and Testing (2003, methodology): “, heuristic search), checking of temporal properties, and partial order and symmetry reductions; – Automating non-isomorphic test input generation to satisfy a testing criterion for programs with complex inputs and preconditions; – A series of examples and a prototype implementation in Java, that us”
A Survey of Automated Techniques for Formal Software Verification (2008, background): “Instead of unwinding the entire transition relation, each loop is unwound separately.”
Compositional dynamic test generation (2007, methodology): “Actually, DART can be viewed [GK05] as one way of combining static (interface extraction, symbolic execution) and dynamic (testing, run-time checking) program analysis with model-checking techniques (systematic state-space exploration) in order to address one of the main limitations of previous dyna”
Program synthesis by sketching (2008, background): “Modern model checking tools, for example, are now able to expose errors in complex routines with relatively little user e ort [7,21,37,68].”
Practical verification of decision-making in agent-based autonomous systems (2013, methodology): “The Java Pathfinder (JPF) system (Visser et al. 2003) carries out formal verification of Java programs in this way by analysing all the possible execution paths.”
Context-Bounded Model Checking of Concurrent Software (2005, background): “A number of model checkers have been developed for concurrent software [17, 14, 29, 9, 26, 18, 30].”
SOBER: statistical model-based bug localization (2005, methodology): “Static analysis can detect program defects through checking either a well-specified program model [4] or real code directly [23, 17].”
Extended static checking for Java (2002, methodology): “Other tools that verify properties of software systems using finite-state models are Bandera [5] and Java PathFinder 2 [46].”
Synthesizing Monitors for Safety Properties (2002, background): “Model checking of programs has received an increased attention from the formal methods community within the last couple of years, and several systems have emerged that can directly model check source code, such as Java and C [7, 21, 3, 12, 2, 17].”
Test input generation with java PathFinder (2004, methodology): “More recently the application of model checking to the analysis of software programs has also come to the fore [7,15,27,43].”
A NICE Way to Test OpenFlow Applications (2012, methodology): “Next, we contrast NICE-MC with two state-of-the-art model checkers, SPIN [12] and JPF [13].”
Cosette: An Automated Prover for SQL (2017, background): “This strategy has been applied in numerous real-world scenarios (e.g., [34, 12]).”
Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III (2019, neutral): “There have been a number of related initiatives with the goal of increasing awareness for the scientific method of evaluating tools in a competition-based fashion, like the COMPARE workshop on Comparative Empirical Evaluation of Reasoning Systems [63], the Dagstuhl seminar on Evaluating Software Ver”