Higher-order constrained horn clauses for verification

Higher-order constrained horn clauses for verification

Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally h...

书目详细资料
Main Authors:	Cathcart Burn, T, Ong, C, Ramsay, S
格式:	Journal article
语言:	English
出版:	Association for Computing Machinery 2017

相似书籍

Higher-order constrained Horn clauses for higher-order program verification
由: Jochems, J
出版: (2020)

Initial limit Datalog: a new extensible class of decidable constrained Horn clauses
由: Cathcart Burn, T, et al.
出版: (2021)

Decomposition by tree dimension in Horn clause verification
由: Bishoksan Kafle, et al.
出版: (2015-12-01)

Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
由: Qi Zhou, et al.
出版: (2018-09-01)

Removing Unnecessary Variables from Horn Clause Verification Conditions
由: Emanuele De Angelis, et al.
出版: (2016-07-01)

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
由: Emanuele De Angelis, et al.
出版: (2019-07-01)

Solving non-linear Horn clauses using a linear Horn clause solver
由: Bishoksan Kafle, et al.
出版: (2016-07-01)

Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
由: Bishoksan Kafle, et al.
出版: (2014-12-01)

Hierarchical State Machines as Modular Horn Clauses
由: Pierre-Loïc Garoche, et al.
出版: (2016-07-01)

Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
由: Emanuele De Angelis, et al.
出版: (2019-08-01)

The order of clauses
由: Luka Vukojević
出版: (2009-01-01)

Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
由: Ekaterina Komendantskaya Dr, et al.
出版: (2018-09-01)

Verifying higher-order functional programs with pattern-matching algebraic data types
由: Ong, C, et al.
出版: (2010)

Verifying Higher−Order Functional Programs with Pattern Matching Algebraic Data Types
由: Ong, C, et al.
出版: (2011)

Higher Order Logic and Hardware Verification
由: Melham, T
出版: (1993)

Generalising submodularity and horn clauses: Tractable optimization problems defined by tournament pair multimorphismsa
由: Cohen, D, et al.
出版: (2008)

Generalising Submodularity and Horn Clauses: Tractable optimization problems defined by tournament pair multimorphisms
由: Jeavons, P, et al.
出版: (2006)

Generalising submodularity and Horn clauses: tractable optimization problems defined by tournament pair multimorphisms
由: Cohen, D, et al.
出版: (2008)

A Traversal Based Algorithm for Higher−Order Model Checking
由: Neatherway, R, et al.
出版: (2012)

Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types
由: Ong, C, et al.
出版: (2011)

Constraining higher order gravities with subregion duality
由: Elena Cáceres, et al.
出版: (2019-11-01)

Efficient CTL Verification via Horn Constraints Solving
由: Tewodros A. Beyene, et al.
出版: (2016-07-01)

Hardware Verification using Higher−Order Logic
由: Camilleri, A, et al.
出版: (1986)

Hardware Verification using Higher−Order Logic
由: Camilleri, A, et al.
出版: (1987)

A type−directed abstraction refinement approach to higher−order model checking
由: Ramsay, S, et al.
出版: (2014)

Strictness Analysis for Higher Order Functions
由: Burn, G, et al.
出版: (1986)

α-Resolution Method for Lattice-valued Horn Generalized Clauses in Lattice-valued Propositional Logic Systems
由: Weitao Xu, et al.
出版: (2015-12-01)

Model checking liveness properties of higher-order functional programs
由: Lester, MM, et al.
出版: (2011)

The Theory of Strictness Analysis for Higher Order Functions
由: Burn, G, et al.
出版: (1986)

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic
由: Melham, T
出版: (1989)

Higher-order olfactory neurons in the lateral horn support odor valence and odor identity coding in Drosophila
由: Sudeshna Das Chakraborty, et al.
出版: (2022-05-01)

Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
由: Chunna Zhao, et al.
出版: (2022-08-01)

Clause order in sentences containing a since- subordinate
由: Bénédicte GUILLAUME
出版: (2013-12-01)

Constituent order in Serbian Sign Language declarative clauses
由: Adam Charles Schembri, et al.
出版: (2021-04-01)

Higher-order moving mesh methods for PDE-constrained shape optimization
由: Paganini, A, et al.
出版: (2018)

Optimal Design and Experimental Verification of Ultrasonic Cutting Horn for Ceramic Composite Material
由: Mibbeum Hahn, et al.
出版: (2021-02-01)

Adverbial causal clauses as relative clauses
由: Emanuela Sanfelici, et al.
出版: (2024-03-01)

SLD-resolution reduction of second-order horn fragments
由: Tourret, S, et al.
出版: (2019)

Optimal verification of the Bell state and Greenberger–Horne–Zeilinger states in untrusted quantum networks
由: Yun-Guang Han, et al.
出版: (2021-11-01)

Rules of exclusion clause : the site investigation clause /
由: Shazwana Buang, 1979- author, et al.
出版: (2017)