Product programs in the wild: retrofitting program verifiers to check information flow security
DOI10.1007/978-3-030-81685-8_34zbMATH Open1493.68106OpenAlexW3184432289MaRDI QIDQ832225FDOQ832225
Authors: N. E. Zubov 
Publication date: 25 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_34
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- Simplify: a theorem prover for program checking
- Why3 -- where programs meet provers
- Regression verification for unbalanced recursive functions
- Title not available (Why is that?)
- Resources, concurrency, and local reasoning
- A Basis for Verifying Multi-threaded Programs
- Secure information flow by self-composition
- Simple relational correctness proofs for static analyses and program transformations
- Towards modularly comparing programs using automated theorem provers
- Static Analysis
- Modular product programs
- Viper: a verification infrastructure for permission-based reasoning
- Beyond 2-safety: asymmetric product programs for relational program verification
- \textsc{SecCSL}: security concurrent separation logic
- Property directed self composition
Cited In (3)
Uses Software
This page was built for publication: Product programs in the wild: retrofitting program verifiers to check information flow security
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832225)
