scientific article; zbMATH DE number 7453190

MaRDI QIDQ5020649zbMATH OpenFDO

Authors John P. Gallagher, Manuel Hermenegildo, Bishoksan Kafle, Maximiliano Klemen, P. López-García, J. F. Morales

Publication date 6 January 2022

Full work available at URL https://arxiv.org/abs/2008.02931, http://eptcs.web.cse.unsw.edu.au/paper.cgi?VPTHCVS2020.4

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 3860370 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 108368 (Why is no real title available?)
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• A New Algorithm for Identifying Loops in Decompilation
• A general framework for static profiling of parametric resource usage
• An axiomatic basis for computer programming
• Fast Algorithms for Solving Path Problems
• Horn clause solvers for program verification
• Horn clauses as an intermediate representation for program analysis and transformation
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• Mechanized semantics for the clight subset of the C language
• Most specific logic programs
• Offline specialisation in Prolog using a hand-written compiler generator
• STACS 87. 4th annual symposium on theoretical aspects of computer science, Passau, Federal Republic of Germany, February 19--21, 1987. Proceedings
• Synthesis and transformation of logic programs using unfold/fold proofs
• The origins of structural operational semantics
• Tree dimension in verification of constrained Horn clauses

Cited in

(4)

• Deriving Pretty-Big-Step Semantics from Small-Step Semantics
• VeriFly: On-the-fly Assertion Checking via Incrementality
• Parallel Logic Programming: A Sequel
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

Describes a project that uses

Uses Software

• LOGEN
• Ciao
• CiaoPP
• SeaHorn
• RAHFT
• JayHorn

This page was built for publication:

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