Unifying type checking and property checking for low-level code

DOI10.1145/1480881.1480921MaRDI QIDQ5261528zbMATH OpenOpenAlexFDO

Authors Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, 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

assertion checkingdecision procedurelow-level codeproperty checkingSMT solvertype checking

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2087533
• Low-level liquid types
• Hybrid type checking
• Programming Languages and Systems
• scientific article; zbMATH DE number 1949628

Cited in

(5)

• Partitioned memory models for program analysis
• ExplainHoudini: making Houdini inference transparent
• scientific article; zbMATH DE number 2087533 (Why is no real title available?)
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Heaps and Data Structures: A Challenge for Automated Provers

Describes a project that uses

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

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