Lockstep composition for unbalanced loops

DOI10.1007/978-3-031-30820-8_18MaRDI QIDQ6536133zbMATH OpenFDO

Authors Ameer Hamza, Grigory Fedyukovich

Publication date 5 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30820-8_18

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Program equivalence checking by two-tape automata
• Property directed equivalence via abstract simulation
• Regression verification for unbalanced recursive functions
• Efficient equivalence-checking algorithms for procedural programs in progressive semigroup gateway models

Cites work

• A self-certifying compilation framework for WebAssembly
• Abstract Semantic Differencing for Numerical Programs
• Automating regression verification of pointer programs by predicate abstraction
• Constraint-based relational verification
• Inference rules for proving the equivalence of recursive procedures
• Modular demand-driven analysis of semantic difference for program versions
• Property directed self composition
• Quantified invariants via syntax-guided synthesis
• Regression verification for unbalanced recursive functions
• Relational verification through Horn clause transformation
• Synchronizing constrained Horn clauses
• Transition power abstractions for deep counterexample detection

This page was built for publication: Lockstep composition for unbalanced loops

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