scientific article; zbMATH DE number 7440192

zbMath1482.68141arXiv1607.04459MaRDI QIDQ5015369

Bishoksan Kafle, John P. Gallagher, Pierre Ganty

Publication date: 7 December 2021

Full work available at URL: https://arxiv.org/abs/1607.04459

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Solving constrained Horn clauses over algebraic data types ⋮ Tree dimension in verification of constrained Horn clauses

Uses Software

• LOGEN
• FLATA
• Yices
• PPL
• Princess
• Eldarica
• HSF
• VeriMAP

Cites Work

• Unnamed Item
• Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11--18, 2015. Proceedings
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• Convergence of Newton's method over commutative semirings
• Linearisability on Datalog programs
• Transformation by interpreter specialisation
• Parikh's theorem: a simple and direct automaton construction
• Fast offline partial evaluation of logic programs
• An overview of Ciao and its design philosophy
• On Fixed Point Equations over Commutative Semirings
• Proving correctness of imperative programs by linearizing constrained Horn clauses
• Underapproximation of Procedure Summaries for Integer Programs
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints