Automated Deduction – CADE-20
From MaRDI portal
Publication:5394619
DOI10.1007/11532231zbMath1102.03303OpenAlexW2485416161MaRDI QIDQ5394619
Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
Publication date: 1 November 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11532231
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (11)
Decision Procedures for Region Logic ⋮ Program verification with interacting analysis plugins ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Decision procedures for term algebras with integer constraints ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Certified Reasoning with Infinity ⋮ Counting Constraints in Flat Array Fragments ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity ⋮ Efficient automated reasoning about sets and multisets with cardinality constraints
Uses Software
This page was built for publication: Automated Deduction – CADE-20
