Combining model checking and testing

DOI10.1007/978-3-319-10575-8_19MaRDI QIDQ3176377zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 2038698
• Introduction to model checking
• scientific article; zbMATH DE number 910719
• Model checking at IBM
• Software Model Checking: Searching for Computations in the Abstract or the Concrete

Cites work

• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• scientific article; zbMATH DE number 1670567 (Why is no real title available?)
• scientific article; zbMATH DE number 1670793 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A general-purpose algorithm for analyzing concurrent programs
• An axiomatic basis for computer programming
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Bounded model checking using satisfiability solving
• CCured, type-safe retrofitting of legacy code
• Compositional may-must program analysis: unleashing the power of alternation
• Demand-Driven Compositional Symbolic Execution
• Dynamic partial-order reduction for model checking software
• Experimental evaluation of verification and validation tools on Martian Rover software
• FM 2005: Formal Methods
• Formal Approaches to Software Testing
• Framework for testing multi‐threaded Java programs
• Generating Path Conditions for Timed Systems
• Guarded commands, nondeterminacy and formal derivation of programs
• Information reuse for multi-goal reachability analyses
• Model checking, testing and verification working together
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Sound and complete monitoring of sequential consistency for relaxed memory models
• Symbolic Testing and the DISSECT Symbolic Evaluation System
• Symbolic execution and program testing
• Symbolic model checking: \(10^{20}\) states and beyond
• Tools and Algorithms for the Construction and Analysis of Systems
• Verifying time partitioning in the DEOS scheduling kernel

Cited in

(8)

• Formal Approaches to Software Testing
• scientific article; zbMATH DE number 2102699 (Why is no real title available?)
• scientific article; zbMATH DE number 2038698 (Why is no real title available?)
• scientific article; zbMATH DE number 1956475 (Why is no real title available?)
• Diagnosis and testing: how is their relation? Can they be combined?
• Software Model Checking: Searching for Computations in the Abstract or the Concrete
• Combining Model Checking and Deduction
• Theoretical Aspects of Computing - ICTAC 2004

Describes a project that uses

Uses Software

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

This page was built for publication: Combining model checking and testing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176377)