Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables

DOI10.1007/978-3-642-02949-3_11MaRDI QIDQ3637253zbMATH OpenOpenAlexFDO

Authors Nicolas Rapin

Publication date 7 July 2009

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02949-3_11

zbMATH Keywords

input-output symbolic transition systemslinear temporal logicsymbolic executionverification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Module checking
• Symbolic model checking: \(10^{20}\) states and beyond
• Symbolic Execution Techniques for Test Purpose Definition
• Algebraic Methodology and Software Technology
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

Cites work

• A classification of symbolic transition systems
• A polynomial algorithm for testing diagnosability of discrete-event systems
• Computer Aided Verification
• Computer Aided Verification
• Formal Approaches to Software Testing
• scientific article; zbMATH DE number 1670791 (Why is no real title available?)
• scientific article; zbMATH DE number 1956610 (Why is no real title available?)
• scientific article; zbMATH DE number 2079824 (Why is no real title available?)
• scientific article; zbMATH DE number 1796145 (Why is no real title available?)
• Symbolic execution and program testing
• Symbolic Execution Techniques for Refinement Testing
• Symbolic Execution Techniques for Test Purpose Definition

Cited in

(2)

• Unbeast: Symbolic Bounded Synthesis
• Symbolic execution of transition systems with function summaries

Describes a project that uses

Uses Software

• AGATHA
• Omega
• TREX

This page was built for publication: Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables

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