Combining Model Checking and Testing

DOI10.1007/978-3-319-10575-8_19zbMath1392.68250OpenAlexW2472899067MaRDI QIDQ3176377

Patrice Godefroid, Koushik Sen

Publication date: 20 July 2018

Published in: Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_19

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Combining Model Checking and Deduction

Uses Software

• CUTE
• veriSoft
• CalFuzzer
• SLAM
• z3
• KLEE
• ISP
• PathCrawler
• ADL
• DART
• Pex
• Java PathFinder
• Bandera
• Boogie
• CESAR
• ConTest
• JPAX
• CCured
• BitBlaze
• SpecExplorer
• JPF-SE
• MODIST
• YOGI
• Snugglebug
• Looper
• CATG
• Jalangi
• jCUTE
• STP
• Con2colic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying time partitioning in the DEOS scheduling kernel
• Symbolic model checking: \(10^{20}\) states and beyond
• Experimental evaluation of verification and validation tools on Martian Rover software
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Model checking, testing and verification working together
• Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
• A general-purpose algorithm for analyzing concurrent programs
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Guarded commands, nondeterminacy and formal derivation of programs
• Symbolic execution and program testing
• Symbolic Testing and the DISSECT Symbolic Evaluation System
• Framework for testing multi‐threaded Java programs
• CCured
• Compositional may-must program analysis
• Dynamic partial-order reduction for model checking software
• Information Reuse for Multi-goal Reachability Analyses
• Generating Path Conditions for Timed Systems
• Demand-Driven Compositional Symbolic Execution
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems
• FM 2005: Formal Methods
• Formal Approaches to Software Testing
• Bounded model checking using satisfiability solving