Unifying type checking and property checking for low-level code

DOI10.1145/1480881.1480921zbMath1315.68086OpenAlexW2111050128MaRDI QIDQ5261528

Jeremy Condit, Shuvendu K. Lahiri, Brian Hackett, Shaz Qadeer

Publication date: 3 July 2015

Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1480881.1480921

zbMATH Keywords

decision proceduretype checkingSMT solverproperty checkinglow-level codeassertion checking

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Partitioned Memory Models for Program Analysis ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ ExplainHoudini: Making Houdini Inference Transparent

Uses Software

• Coq
• SMT-LIB
• Spec#
• z3
• Boogie
• Cyclone
• CCured
• HAVOC

This page was built for publication: Unifying type checking and property checking for low-level code