Heaps and Data Structures: A Challenge for Automated Provers

DOI10.1007/978-3-642-22438-6_15zbMath1341.68182OpenAlexW146004970MaRDI QIDQ5200023

Sascha Böhme, Michał Moskal

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_15

Mathematics Subject Classification ID

Data structures (68P05)

Related Items (3)

A formal semantics of the GraalVM intermediate representation ⋮ Partitioned Memory Models for Program Analysis ⋮ On interpolation in automated theorem proving

Uses Software

• Dafny
• OTTER
• VAMPIRE
• SMT-LIB
• SPASS
• TPTP
• Yices
• cvc3
• z3
• ESC/Java
• ESC4
• VCC
• Boogie
• E Theorem Prover
• VACID-0

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The logic of aliasing
• Isabelle/HOL. A proof assistant for higher-order logic
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Faster and more complete extended static checking for the Java modeling language
• Dafny: An Automatic Program Verifier for Functional Correctness
• Unifying type checking and property checking for low-level code
• New results on rewrite-based satisfiability procedures
• Automated Reasoning

This page was built for publication: Heaps and Data Structures: A Challenge for Automated Provers