Unifying type checking and property checking for low-level code

DOI10.1145/1480881.1480921zbMATH Open1315.68086OpenAlexW2111050128MaRDI QIDQ5261528FDOQ5261528

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

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

Recommendations

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

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)

Cited In (5)

• Heaps and Data Structures: A Challenge for Automated Provers
• ExplainHoudini: Making Houdini Inference Transparent
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Title not available (Why is that?)
• Partitioned Memory Models for Program Analysis

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)