scientific article; zbMATH DE number 1956607

MaRDI QIDQ4417955zbMATH OpenFDO

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

Publication date 30 July 2003

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)

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

Describes a project that uses

Uses Software

• Bandera
• Korat
• NuSMV
• SPIN
• veriSoft

This page was built for publication:

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