A Data Driven Approach for Algebraic Loop Invariants
From MaRDI portal
Publication:5326308
DOI10.1007/978-3-642-37036-6_31zbMath1381.68061MaRDI QIDQ5326308
Bharath Hariharan, Saurabh Gupta, Rahul Sharma, Percy Liang, Aditya V. Nori, Alex Aiken
Publication date: 5 August 2013
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37036-6_31
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Sharper and Simpler Nonlinear Interpolants for Program Verification, ICE-based refinement type discovery for higher-order functional programs, Invariant inference with provable complexity from the monotone theory, SAT-based invariant inference and its relation to concept learning, From invariant checking to invariant inference using randomized search, Constraint-based relational verification, Relational program reasoning using compiler IR, Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses, A learning-based approach to synthesizing invariants for incomplete verification engines, Counterexample- and simulation-guided floating-point loop invariant synthesis, Algebra-based synthesis of loops and their invariants (invited paper), Automatic proving or disproving equality loop invariants based on finite difference techniques, IC3 - Flipping the E in ICE, Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
Uses Software