LMS-Verify: abstraction without regret for verified systems programming

DOI10.1145/3009837.3009867zbMATH Open1380.68080OpenAlexW2562397426WikidataQ131121844 ScholiaQ131121844MaRDI QIDQ5370919FDOQ5370919

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

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

zbMATH Keywords

verificationsecuritycontractsLMSblamememory safetyFrama-CDSLs

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Cited In (3)

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

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)