Unbounded procedure summaries from bounded environments

DOI10.1007/978-3-030-67067-2_14MaRDI QIDQ2234080zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Summary-based inter-procedural analysis via modular trace refinement
• SMT-based model checking for recursive programs
• Computing Procedure Summaries for Interprocedural Analysis
• Mechanical verification of mutually recursive procedures
• Programming Languages and Systems

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 1865733 (Why is no real title available?)
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• Automating induction for solving Horn clauses
• Compositional may-must program analysis: unleashing the power of alternation
• Function summarization modulo theories
• Generalized property directed reachability
• HoIce: an ICE-based non-linear Horn clause solver
• Interpolation and SAT-based model checking.
• Learning inductive invariants by sampling from frequency distributions
• Maximal specification synthesis
• Mining specifications
• Quantified invariants via syntax-guided synthesis
• Refinement of Trace Abstraction
• SAT-Based Model Checking without Unrolling
• SMT-based model checking for recursive programs
• Satisfiability modulo theories
• Static contract checking with abstract interpretation
• Synthesis of interface specifications for Java classes
• Unbounded procedure summaries from bounded environments

Cited in

(4)

• Unbounded procedure summaries from bounded environments
• Summary-based inter-procedural analysis via modular trace refinement
• Efficient modular SMT-based model checking of pointer programs
• Function summarization modulo theories

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

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