Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?

DOI10.1007/978-3-642-18070-5_3MaRDI QIDQ3067532zbMATH OpenOpenAlexFDO

Authors Davide Ancona, Andrea Corradi, Giovanni Lagorio, Ferruccio Damiani

Publication date 21 January 2011

Published in Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-18070-5_3

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas
• Type Inference by Coinductive Logic Programming
• scientific article; zbMATH DE number 549959
• Static analysis, abstract interpretation and verification in (constraint logic) programming
• scientific article; zbMATH DE number 2086518

Cites work

• Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coinductive Logic Programming
• Constraint Handling Rules
• Fundamental properties of infinite trees
• HM(X) type inference is CLP(X) solving
• Idealized coinductive type systems for imperative object-oriented programs
• Intersection and union types: Syntax and semantics
• Type Inference by Coinductive Logic Programming
• Verifying complex continuous real-time systems with coinductive CLP(R)

Cited in

(4)

• Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?
• Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas
• Idealized coinductive type systems for imperative object-oriented programs
• Static single information form for abstract compilation

Describes a project that uses

Uses Software

• Featherweight Java

This page was built for publication: Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?

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