Software Verification with BLAST

By Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, G. Sutre. SPIN, 2003

527 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/79f27227130db80a93d323364db1e195c382bded

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. Tao Xie
2. Toby C. Murray
3. Willem Visser
4. Thomas Sewell
5. Kai Engelhardt
6. Jian Pei
7. Sarfraz Khurshid
8. David Notkin

In Computational Theory and Mathematics

1. Koushik Sen
2. Darko Marinov
3. Corina S. Pasareanu
4. Sarfraz Khurshid
5. Willem Visser
6. Tao Xie
7. Wolfram Schulte
8. David Notkin

In Software

1. Corina S. Pasareanu
2. Koushik Sen
3. Darko Marinov
4. Sarfraz Khurshid
5. Willem Visser
6. Tao Xie
7. Wolfram Schulte
8. David Notkin

Citations in the corpus

• Comprehensive formal verification of an OS microkernel (2014, methodology): “Model checking in the OS space includes SLAM [Ball and Rajamani 2001] and BLAST [Henzinger et al. 2003].”
• Mining API patterns as partial orders from source code: from usage scenarios to specifications (2007, methodology): “Software veri.cation with BLAST.”
• seL4: Formal Verification of an OS Kernel (2009, methodology): “Model checking in the OS space includes SLAM [6] and BLAST [34].”
• 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].”
• Abstract Regular Model Checking (2004, methodology): “, in tools for software model checking like Slam [6], Magic [13], or Blast [19].”
• Combining unit-level symbolic execution and system-level concrete execution for testing nasa software (2008, background): “Unlikeprevioussymbolicexecution approaches(e.g., our ownprevious approach[27,5] but also[19,32]) that work by code instrumentation, this new framework does not re­quire such instrumentation, but instead implements a non­standard interpreter ofbytecodes.”
• 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].”
• Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (2005, methodology): “Recently, tools such as SLAM [4,2] and Blast [17,7] were adapted for test generation.”
• Exploring Multiple Execution Paths for Malware Analysis (2007, unknown): “For example, model checking tools [10, 17, 18] translate programs into finite state machines and then reason whether certain properties hold on these automata.”
• seL4: formal verification of an OS kernel (2009, methodology): “Model checking in the OS space includes SLAM [6] and BLAST [34].”
• 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].”