A new acceleration-based combination framework for array properties

DOI10.1007/978-3-319-24246-0_11zbMATH Open1471.68232OpenAlexW2295800466MaRDI QIDQ2964461FDOQ2964461

Natasha Sharygina, Francesco Alberti, Silvio Ghilardi

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_11

Recommendations

• Booster: an acceleration-based verification framework for array programs
• Definability of accelerated relations in a theory of arrays and its applications
• Towards SMT Model Checking of Array-Based Systems
• Decision procedures for flat array properties
• Artificial Intelligence and Symbolic Computation

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Decidability of theories and sets of sentences (03B25)

Cites Work

• Booster: An Acceleration-Based Verification Framework for Array Programs
• Mathematical logic.
• Definability of Accelerated Relations in a Theory of Arrays and Its Applications
• Decision procedures for flat array properties
• LOGICAL THEORIES OF ONE-PLACE FUNCTIONS ON THE SET OF NATURAL NUMBERS
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Title not available (Why is that?)
• A Logic of Singly Indexed Arrays
• MCMT: A Model Checker Modulo Theories
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Fast Acceleration of Ultimately Periodic Relations
• Iterating Octagons
• On iterating linear transformations over recognizable sets of integers

Uses Software

• FLATA
• Mcmt

This page was built for publication: A new acceleration-based combination framework for array properties

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