Decision procedures for flat array properties

DOI10.1007/s10817-015-9323-7zbMath1356.03049OpenAlexW2017654412MaRDI QIDQ287272

Natasha Sharygina, Silvio Ghilardi, Francesco Alberti

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://doc.rero.ch/record/331489/files/10817_2015_Article_9323.pdf

zbMATH Keywords

arraysquantifiersSMTdecision procedures

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Data structures (68P05)

Related Items

Decision procedures for flat array properties, NP satisfiability for arrays as powers, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Cardinality constraints for arrays (decidability results and applications), A New Acceleration-Based Combination Framework for Array Properties, On algebraic array theories, An array content static analysis based on non-contiguous partitions, Higher-order quantifier elimination, counter simulations and fault-tolerant systems

Uses Software

• SMT-LIB
• z3
• SIMPLIFY
• veriT
• CVC4
• Mcmt
• SAFARI
• Booster

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The 2013 evaluation of SMT-COMP and SMT-LIB
• Decision procedures for flat array properties
• An extension of lazy abstraction with interpolation for programs with arrays
• Combining nonstably infinite theories
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Definability of Accelerated Relations in a Theory of Arrays and Its Applications
• Lazy Abstraction with Interpolants for Arrays
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• LOGICAL THEORIES OF ONE-PLACE FUNCTIONS ON THE SET OF NATURAL NUMBERS
• Booster: An Acceleration-Based Verification Framework for Array Programs
• Simplify: a theorem prover for program checking
• Fluid Updates: Beyond Strong vs. Weak Updates
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Array Abstractions from Proofs
• On Local Reasoning in Verification
• What Else Is Decidable about Integer Arrays?
• A Logic of Singly Indexed Arrays
• Computer Aided Verification
• MCMT: A Model Checker Modulo Theories
• Lazy Abstraction with Interpolants
• Verification, Model Checking, and Abstract Interpretation
• Flat Parametric Counter Automata