Gradual program verification

DOI10.1007/978-3-319-73721-8_2MaRDI QIDQ3296319zbMATH OpenOpenAlexFDO

Authors Johannes Bader, Jonathan Aldrich, Éric Tanter

Publication date 7 July 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-73721-8_2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Gradual refinement types
• Abstracting gradual typing
• Gradual type theory
• scientific article; zbMATH DE number 4024753
• Gradual type-and-effect systems

Cited in

(8)

• Mostly sound type system improves a foundational program verifier
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Collaborative verification and testing with explicit assumptions
• Lightweight static capabilities
• Traits: correctness-by-construction for free
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Gradual tensor shape checking
• Gradual refinement types

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Gradual program verification

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