Aligators for Arrays (Tool Paper)

DOI10.1007/978-3-642-16242-8_25MaRDI QIDQ4933316zbMATH OpenOpenAlexFDO

Authors Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko, Thomas A. Henzinger

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16242-8_25

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Recommendations

• scientific article; zbMATH DE number 426143
• F-arrays, implementation and applications
• Algorithmic analysis of array-accessing programs
• Algorithmic Analysis of Array-Accessing Programs
• Algorithms for assignment problems on an array processor
• Analysis of distributed systems by array algebra
• Synthesizing linear array algorithms from nested FOR loop algorithms
• Algebraic techniques for covering arrays and related structures

Cited in

(7)

• Aligator.jl -- a Julia package for loop invariant generation
• SMT-based array invariant generation
• Invariant and type inference for matrices
• Verifying array manipulating programs with full-program induction
• Quantified invariants via syntax-guided synthesis
• Automatic program instrumentation for automatic verification
• A program instrumentation framework for automatic verification

Describes a project that uses

Uses Software

• Mathematica
• Valigator
• z3
• OCaml
• Aligators
• InvGen

This page was built for publication: Aligators for Arrays (Tool Paper)

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