Generalized symbolic execution for model checking and testing

DOI10.1007/3-540-36577-X_40MaRDI QIDQ4417955zbMATH OpenFDO

Authors Sarfraz Khurshid, Willem Visser, Corina S. Păsăreanu

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2619/26190553.htm

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

• Model Checking Software
• Model Checking Software
• Symbolic model checking of software
• Symbolic execution formally explained
• Enhancing symbolic execution of heap-based programs with separation logic for test input generation

Cited in

(32)

• A symbolic operational semantics for TESL -- with an application to heterogeneous system testing
• Symbolic execution based on language transformation
• The dependence condition graph: precise conditions for dependence between program points
• A local approach for temporal model checking of Java bytecode
• TASS: the toolkit for accurate scientific software
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• The application of hypergroups in symbolic executions and finite automata
• Symbolic partial-order execution for testing multi-threaded programs
• A formal model for detecting bugs by symbolic execution of programs
• Exact heap summaries for symbolic execution
• Loop invariant symbolic execution for parallel programs
• Testing state design pattern implementations with symbolic execution
• Collective assertions
• Combining model checking and testing
• Model Checking MSVL Programs Based on Dynamic Symbolic Execution
• Enhancing symbolic execution of heap-based programs with separation logic for test input generation
• Symbolic and on the Fly Testing with Real-Time Observers
• A Self-Checking Generalized Prediction Checker and Its Use for Built-In Testing
• Symbolic execution of Reo circuits using constraint automata
• A dynamic logic for deductive verification of multi-threaded programs
• Model Checking Using Generalized Testing Automata
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• A generic framework for symbolic execution: a coinductive approach
• Unit checking: symbolic model checking for a unit of code
• Model Checking Software
• Demand-Driven Compositional Symbolic Execution
• Combining test case generation and runtime verification
• Model Checking Software
• Towards efficient data-flow test data generation
• Concolic testing heap-manipulating programs
• Verifying time partitioning in the DEOS scheduling kernel
• CPBPV: a constraint-programming framework for bounded program verification

Describes a project that uses

Uses Software

• Bandera
• veriSoft
• NuSMV
• Korat
• SPIN

This page was built for publication: Generalized symbolic execution for model checking and testing

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