Verifying pointer and string analyses with region type systems

DOI10.1016/J.CL.2013.01.001MaRDI QIDQ2014831zbMATH OpenOpenAlexFDO

Authors Lennart Beringer, Robert Grabowski, Martin Hofmann

Publication date 16 June 2014

Published in Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.cl.2013.01.001

zbMATH Keywords

formal verificationobject-oriented languagespointer alias analysisregion type systemstring analysis

Mathematics Subject Classification ID

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

Recommendations

• Verifying pointer and string analyses with region type systems
• Region analysis for deductive verification of C programs
• scientific article; zbMATH DE number 1948396
• Pointer logic for verification of pointer programs
• Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
• Automated verification of recursive programs with pointers
• Automating regression verification of pointer programs by predicate abstraction
• Completeness and expressiveness of pointer program verification by separation logic

Cites work

• A Certified Lightweight Non-interference Java Bytecode Verifier
• Certification Using the Mobius Base Logic
• scientific article; zbMATH DE number 1956461 (Why is no real title available?)
• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• Modular control-flow analysis with rank 2 intersection types
• Programming Languages and Systems
• Region-based memory management
• Semi-sparse flow-sensitive pointer analysis
• Types and programing languages
• Verifying pointer and string analyses with region type systems

Cited in

(4)

• Verifying pointer and string analyses with region type systems
• scientific article; zbMATH DE number 1231585 (Why is no real title available?)
• Enforcing Programming Guidelines with Region Types and Effects
• Inferring region types via an abstract notion of environment transformation

Describes a project that uses

Uses Software

• TAJ
• Featherweight Java

This page was built for publication: Verifying pointer and string analyses with region type systems

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