Unbounded procedure summaries from bounded environments

DOI10.1007/978-3-030-67067-2_14zbMath1472.68093OpenAlexW3120731329MaRDI QIDQ2234080

Lauren Pick, Grigory Fedyukovich, Aarti Gupta

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_14

zbMATH Keywords

program verificationmodular verificationbounded environmentsCHC solversprocedure summaries

Mathematics Subject Classification ID

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

Related Items (1)

Unbounded procedure summaries from bounded environments

Cites Work

• SMT-based model checking for recursive programs
• Automating induction for solving Horn clauses
• Learning inductive invariants by sampling from frequency distributions
• Unbounded procedure summaries from bounded environments
• Maximal specification synthesis
• Generalized Property Directed Reachability
• Static Contract Checking with Abstract Interpretation
• SAT-Based Model Checking without Unrolling
• Satisfiability Modulo Theories
• Refinement of Trace Abstraction
• Mining specifications
• Function Summarization Modulo Theories
• Compositional may-must program analysis
• Synthesis of interface specifications for Java classes
• Computer Aided Verification
• HoIce: an ICE-based non-linear Horn clause solver
• Quantified invariants via syntax-guided synthesis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Unbounded procedure summaries from bounded environments