Computing invariants with transformers: experimental scalability and accuracy

DOI10.1016/J.ENTCS.2014.08.003MaRDI QIDQ281287zbMATH OpenOpenAlexWikidataFDO

Authors Vivien Maisonneuve, Olivier Hermant, François Irigoin

Publication date 10 May 2016

Full work available at URL https://doi.org/10.1016/j.entcs.2014.08.003

zbMATH Keywords

transformerbenchmarkmodel checkingabstract interpretationautomatic invariant detectionlinear relation analysisloop invariantstatic program analysis

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

• A new abstraction framework for affine transformers
• A new abstraction framework for affine transformers
• scientific article; zbMATH DE number 1617317
• Verifying Recurrent Neural Networks Using Invariant Inference
• From invariant checking to invariant inference using randomized search
• scientific article; zbMATH DE number 4029728

Cites work

• scientific article; zbMATH DE number 1940300 (Why is no real title available?)
• A modular static analysis approach to affine loop invariants detection
• Combining Widening and Acceleration in Linear Relation Analysis
• Convex invariant refinement by control node splitting: a heuristic approach
• Policy iteration-based conditional termination and ranking functions
• isl: An integer set library for the polyhedral model

Cited in

(4)

• Convex invariant refinement by control node splitting: a heuristic approach
• A new abstraction framework for affine transformers
• A modular static analysis approach to affine loop invariants detection
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• Omega
• ALICe
• PAGAI
• isl
• Aspic

This page was built for publication: Computing invariants with transformers: experimental scalability and accuracy

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