Interleaving Symbolic Execution and Partial Evaluation

DOI10.1007/978-3-642-17071-3_7zbMath1312.68055OpenAlexW1838500763MaRDI QIDQ3066122

Richard Bubel, Reiner Hähnle, Ran Ji

Publication date: 8 January 2011

Published in: Formal Methods for Components and Objects (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Uses Software

• Spec#
• Pex
• VeriFast
• Refal

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mixtus: An automatic partial evaluator for full Prolog
• Predicate Abstraction in a Program Logic Calculus
• Dynamic Logic with Non-rigid Functions
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• The concept of a supercompiler
• Model Checking Software
• Algebraic Methodology and Software Technology
• Generating Unit Tests from Formal Proofs