Model Checking and Testing: Bibliography

Reading groups

Graduate Reading Course on Formal Software Testing and Model Checking 
Study group: formal approaches to software test

Surveys

Issues in Software Testing with Model Checkers by Vadim Okun and Paul E. Black (DSN 2003)
Model Checkers in Software Testing by Paul Ammann, Paul E. Black, and Wei Ding (NIST-IR 2002)
Course project on test generation using model checking (other projects

Test generation by mutations of specifications

Paul E. Black (NIST) Automatic Software Test Generation  Issues in Software Testing with Model Checkers Model Checkers in Software Testing Mutation of Model Checker Specifications  Other Papers
Paul Amann (Georgia Mason U.) Test generation with model checkers

Test generation by formulating coverage criteria as trap properties

Angelo Gargantini (Città Universitaria) Using Model Checking to Generate Tests from Requirements
Connie Heitmeyer (Navy Lab) 
Hyoung Seok Hong (Concordia U.)
Insup Lee (U Penn) Model-Based Test Generation  Run-time monitoring and checking  
Mats P.E. Heimdahl (U. Minnesota) test generation with model checkers
John Rushby (SRI) Generating Efficient Test Sets with a Model Checker
Marsha Chechik (U. Toronto) Model exploration with Model-Checking/Test case generation using query-checking  Reasoning about changing software 
Lihua Xu (UC Irivine) Generating Regression Tests via Model Checking

Test generation by exploiting counterexamples

CnC- Check and Crash: generating tests from ECC/Java counterexamples
Dirk Beyer (UC Berkely) Generating Tests from Counterexamples: generating tests from Blast counterexamples
Tom Ball (MSR) A Theory of Predicate-Complete Test Coverage and Generation: generating tests from SLAM counterexamples

Testing as model checking

Patrice Godefroid (Bell Labs)  VeriSoft
Willem Visser (NASA) NASA JPF

Misc

Henry Muccini (U. L'Aquila)
Jooyong Lee (Aarhus U.)
Ulrik Nyman (Aalborg U.) Distributed model checking/test generation
Juergen Dingel (Queens U) Testing and Model Checking Implicit-Invocation Systems 
Doron A. Peled (U. Warwick) Black-box model checking Invited VISSAS lecture on test case generation
Keijo Heljanko (U. Stuttgart) Testing and Model checking  Testing tools (download)  Bomotest testing tool (download)
William E. Howden (UCSD)   MOCA (Model Oriented Capture Analysis) 
Alexander Pretschner (Technische U.)  Model-based Testing Pretschner  Constraint Based ATDG (within AutoFocus)
Harry Robinson (Google) Model-based testing
Bernhand Steffen (U. Dortmund) Model generation, web testing, regression testing 
A method for the automatic generation of test suites from object models 
Distributed model checking at Utah
Koushik Sen (UIUC) Runtime verification, learning to verify 
Software Testing Researchers  
Magenta - Multi-Agent Systems and Semantic Web Services 
Web Service Engineering project
Web Service Analysis Tool 
TAV-WEB 
Web service testing

Downloadable tools

ATGT: ASM Tests Generation Tool 
SAL automated test generator  
UBET 
TVG TGV UMLAUT Triskell
UCTSystem - test generation based on UML a prototype tool designed to perform automatic test generation from UML requirements.
AFTG tool demo at NIST   
Focuscheck@Iowa State U.
NASA Java PathFinder
Bomotest: a formal conformance testing tool for the ioco-conformance
Verisoft Automatic Interface (VAI) Framework  VeriSoft
CnC- Check and Crash: generating tests from ECC/Java counterexamples
Lever - Learning to Verify Safety Properties
BZ Testing tools
Uppaal
Agedis Tool
Magenta - Multi-Agent Systems and Semantic Web Services 
BPEL4WS LTSA Plug-In  bpel4ws  MSCplugin 
Web Service Analysis Tool

 

Maintained by