LMS-Verify: abstraction without regret for verified systems programming

DOI10.1145/3009837.3009867MaRDI QIDQ5370919zbMATH OpenOpenAlexWikidataFDO

Authors Nada Amin, Tiark Rompf

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

verificationsecuritycontractsLMSblamememory safetyFrama-CDSLs

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• An LTL proof system for runtime verification
• Language-Based Abstraction Refinement for Hybrid System Verification
• Effective abstractions for verification under relaxed memory models
• Effective Abstractions for Verification under Relaxed Memory Models
• Verification of concrete programs with respect to abstract programs

Cited in

(3)

• Unified program generation and verification: a case study on number-theoretic transform
• Embedded domain specific verifiers
• An abstraction algorithm for the verification of level-sensitive latch-based netlists

Describes a project that uses

Uses Software

• BLAST
• ACSL
• Spec#
• OptiML
• Leon
• TreatJS

This page was built for publication: LMS-Verify: abstraction without regret for verified systems programming

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