Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables

DOI10.1007/978-3-642-02949-3_11zbMath1246.68157OpenAlexW1622563620MaRDI QIDQ3637253

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

verificationlinear temporal logicsymbolic executioninput-output symbolic transition systems

Mathematics Subject Classification ID

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

Uses Software

• TREX
• AGATHA
• Omega

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic Execution Techniques for Test Purpose Definition
• Symbolic execution and program testing
• A polynomial algorithm for testing diagnosability of discrete-event systems
• A classification of symbolic transition systems
• Computer Aided Verification
• Symbolic Execution Techniques for Refinement Testing
• Formal Approaches to Software Testing
• Computer Aided Verification

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