Готові списки джерел за темами / Constrained horn clauses

Добірка наукової літератури з теми "Constrained horn clauses"

Автор: Grafiati
Опубліковано: 6 вересня 2023

Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями

Оберіть тип джерела:

Зміст

Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Constrained horn clauses".

Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.

Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.

Статті в журналах з теми "Constrained horn clauses"

1

DE ANGELIS, EMANUELE, FABIO FIORAVANTI, ALBERTO PETTOROSSI, and MAURIZIO PROIETTI. "Proving correctness of imperative programs by linearizing constrained Horn clauses." Theory and Practice of Logic Programming 15, no. 4-5 (July 2015): 635–50. http://dx.doi.org/10.1017/s1471068415000289.

Повний текст джерела
Анотація:
AbstractWe present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form {ϕ}, prog {ψ}, where the assertions ϕ and ψ are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that {ϕ}, prog, {ψ} is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here called LA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of those LA-solving methods. These specifications require the proof of satisfiability of a set PC of constrained Horn clauses that contain nonlinear clauses (that is, clauses with more than one atom in their premise). Then, we present a transformation, called linearization, that converts PC into a set of linear clauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid by LA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.
Стилі APA, Harvard, Vancouver, ISO та ін.
2

KAFLE, BISHOKSAN, JOHN P. GALLAGHER, and PIERRE GANTY. "Tree dimension in verification of constrained Horn clauses." Theory and Practice of Logic Programming 18, no. 2 (March 2018): 224–51. http://dx.doi.org/10.1017/s1471068418000030.

Повний текст джерела
Анотація:
AbstractIn this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCsP, we define a transformation ofPyielding adimension-boundedset of CHCsP≤k. The set of derivations forP≤kconsists of the derivations forPthat have dimension at mostk. We also show how to construct a set of clauses denotedP>kwhose derivations have dimension exceedingk. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.
Стилі APA, Harvard, Vancouver, ISO та ін.
3

DE ANGELIS, EMANUELE, FABIO FIORAVANTI, ALBERTO PETTOROSSI, and MAURIZIO PROIETTI. "Solving Horn Clauses on Inductive Data Types Without Induction." Theory and Practice of Logic Programming 18, no. 3-4 (July 2018): 452–69. http://dx.doi.org/10.1017/s1471068418000157.

Повний текст джерела
Анотація:
AbstractWe address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction.
Стилі APA, Harvard, Vancouver, ISO та ін.
4

Cathcart Burn, Toby, C. H. Luke Ong, and Steven J. Ramsay. "Higher-order constrained horn clauses for verification." Proceedings of the ACM on Programming Languages 2, POPL (January 2018): 1–28. http://dx.doi.org/10.1145/3158099.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
5

KAFLE, BISHOKSAN, JOHN P. GALLAGHER, GRAEME GANGE, PETER SCHACHTE, HARALD SØNDERGAARD, and PETER J. STUCKEY. "An iterative approach to precondition inference using constrained Horn clauses." Theory and Practice of Logic Programming 18, no. 3-4 (July 2018): 553–70. http://dx.doi.org/10.1017/s1471068418000091.

Повний текст джерела
Анотація:
AbstractWe present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set ofunsafeinitial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set ofsafeinitial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.
Стилі APA, Harvard, Vancouver, ISO та ін.
6

Zhou, Qi, David Heath, and William Harris. "Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions." Electronic Proceedings in Theoretical Computer Science 278 (September 12, 2018): 3–18. http://dx.doi.org/10.4204/eptcs.278.3.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
7

Satake, Yuki, Hiroshi Unno, and Hinata Yanagi. "Probabilistic Inference for Predicate Constraint Satisfaction." Proceedings of the AAAI Conference on Artificial Intelligence 34, no. 02 (April 3, 2020): 1644–51. http://dx.doi.org/10.1609/aaai.v34i02.5526.

Повний текст джерела
Анотація:
In this paper, we present a novel constraint solving method for a class of predicate Constraint Satisfaction Problems (pCSP) where each constraint is represented by an arbitrary clause of first-order predicate logic over predicate variables. The class of pCSP properly subsumes the well-studied class of Constrained Horn Clauses (CHCs) where each constraint is restricted to a Horn clause. The class of CHCs has been widely applied to verification of linear-time safety properties of programs in different paradigms. In this paper, we show that pCSP further widens the applicability to verification of branching-time safety properties of programs that exhibit finitely-branching non-determinism. Solving pCSP (and CHCs) however is challenging because the search space of solutions is often very large (or unbounded), high-dimensional, and non-smooth. To address these challenges, our method naturally combines techniques studied separately in different literatures: counterexample guided inductive synthesis (CEGIS) and probabilistic inference in graphical models. We have implemented the presented method and obtained promising results on existing benchmarks as well as new ones that are beyond the scope of existing CHC solvers.
Стилі APA, Harvard, Vancouver, ISO та ін.
8

DE ANGELIS, EMANUELE, FABIO FIORAVANTI, ALBERTO PETTOROSSI, and MAURIZIO PROIETTI. "Predicate Pairing for program verification." Theory and Practice of Logic Programming 18, no. 2 (December 4, 2017): 126–66. http://dx.doi.org/10.1017/s1471068417000497.

Повний текст джерела
Анотація:
AbstractIt is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for constrained Horn clauses (or CHC solvers) based onpredicate abstractionare sometimes unable to verify satisfiability because they look for models that are definable in a given class 𝓐 of constraints, called 𝓐-definable models. We introduce a transformation technique, calledPredicate Pairing, which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an 𝓐-definable model, and hence can be effectively verified by a state-of-the-art CHC solver. In particular, we prove that, under very general conditions on 𝓐, the unfold/fold transformation rules preserve the existence of an 𝓐-definable model, that is, if the original clauses have an 𝓐-definable model, then the transformed clauses have an 𝓐-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an 𝓐-definable modelif and only ifthe original ones have an 𝓐-definable model. Then, we present a strategy, called Predicate Pairing, which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability problem can be solved by looking for 𝓐-definable models. The Predicate Pairing (PP) strategy introduces a new predicate defined by the conjunction of two predicates occurring in the original set of clauses, together with a conjunction of constraints. We will show through some examples that an 𝓐-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We will also present some case studies showing that Predicate Pairing plays a crucial role in the verification ofrelational properties of programs, that is, properties relating two programs (such as program equivalence) or two executions of the same program (such as non-interference). Finally, we perform an experimental evaluation of the proposed techniques to assess the effectiveness of Predicate Pairing in increasing the power of CHC solving.
Стилі APA, Harvard, Vancouver, ISO та ін.
9

K, Hari Govind V., Sharon Shoham, and Arie Gurfinkel. "Solving constrained Horn clauses modulo algebraic data types and recursive functions." Proceedings of the ACM on Programming Languages 6, POPL (January 16, 2022): 1–29. http://dx.doi.org/10.1145/3498722.

Повний текст джерела
Анотація:
This work addresses the problem of verifying imperative programs that manipulate data structures, e.g., Rust programs. Data structures are usually modeled by Algebraic Data Types (ADTs) in verification conditions. Inductive invariants of such programs often require recursively defined functions (RDFs) to represent abstractions of data structures. From the logic perspective, this reduces to solving Constrained Horn Clauses (CHCs) modulo both ADT and RDF. The underlying logic with RDFs is undecidable. Thus, even verifying a candidate inductive invariant is undecidable. Similarly, IC3-based algorithms for solving CHCs lose their progress guarantee: they may not find counterexamples when the program is unsafe. We propose a novel IC3-inspired algorithm Racer for solving CHCs modulo ADT and RDF (i.e., automatically synthesizing inductive invariants, as opposed to only verifying them as is done in deductive verification). Racer ensures progress despite the undecidability of the underlying theory, and is guaranteed to terminate with a counterexample for unsafe programs. It works with a general class of RDFs over ADTs called catamorphisms. The key idea is to represent catamorphisms as both CHCs, via relationification , and RDFs, using novel abstractions . Encoding catamorphisms as CHCs allows learning inductive properties of catamorphisms, as well as preserving unsatisfiabilty of the original CHCs despite the use of RDF abstractions, whereas encoding catamorphisms as RDFs allows unfolding the recursive definition, and relying on it in solutions. Abstractions ensure that the underlying theory remains decidable. We implement our approach in Z3 and show that it works well in practice.
Стилі APA, Harvard, Vancouver, ISO та ін.
10

De Angelis, Emanuele, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. "Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach." Journal of Logic and Computation 32, no. 2 (February 4, 2022): 402–42. http://dx.doi.org/10.1093/logcom/exab090.

Повний текст джерела
Анотація:
Abstract We address the problem of checking the satisfiability of constrained Horn clauses (CHCs) defined on algebraic data types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs defined on ADTs into CHCs where the arguments of the predicates have only basic types, such as integers and booleans. Thus, our technique avoids, during satisfiability checking, the explicit use of proof rules based on induction over the ADTs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates, whose definitions correspond to lemmas that are used when making inductive proofs. We present an algorithm that performs the automatic removal of ADTs by applying the new rule, together with the traditional folding/unfolding rules. We prove that, under suitable hypotheses, the set of the transformed clauses is satisfiable if and only if so is the set of the original clauses. By an experimental evaluation, we show that the use of the new rule significantly improves the effectiveness of ADT removal. We also show that our approach is competitive with respect to tools that extend CHC solvers with the use of inductive rules.
Стилі APA, Harvard, Vancouver, ISO та ін.
Більше джерел

Дисертації з теми "Constrained horn clauses"

1

Reuß, Andreas [Verfasser], Helmut [Akademischer Betreuer] Seidl, and Estaun Francisco Javier [Akademischer Betreuer] Esparza. "Normalization of Horn Clauses with Disequality Constraints / Andreas Reuß. Gutachter: Helmut Seidl ; Francisco Javier Esparza Estaun. Betreuer: Helmut Seidl." München : Universitätsbibliothek der TU München, 2013. http://d-nb.info/1036974731/34.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
2

Reuß, Andreas Verfasser], Helmut [Akademischer Betreuer] [Seidl, and Estaun Francisco Javier [Akademischer Betreuer] Esparza. "Normalization of Horn Clauses with Disequality Constraints / Andreas Reuß. Gutachter: Helmut Seidl ; Francisco Javier Esparza Estaun. Betreuer: Helmut Seidl." München : Universitätsbibliothek der TU München, 2013. http://nbn-resolving.de/urn:nbn:de:bvb:91-diss-20130605-1116533-0-3.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.

Частини книг з теми "Constrained horn clauses"

1

Zlatkin, Ilia, and Grigory Fedyukovich. "Maximizing Branch Coverage with Constrained Horn Clauses." In Tools and Algorithms for the Construction and Analysis of Systems, 254–72. Cham: Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-030-99527-0_14.

Повний текст джерела
Анотація:
AbstractState-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts from symbolic encodings of programs. In this paper, we present a new application to test-case generation: if a block of code is provably unreachable, no test case can be generated allowing to explore other blocks of code. Our new approach uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets our approach to terminate early while guaranteeing maximal coverage. Our implementation called Horntinuum exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art.
Стилі APA, Harvard, Vancouver, ISO та ін.
2

De Angelis, Emanuele, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. "Multiple Query Satisfiability of Constrained Horn Clauses." In Practical Aspects of Declarative Languages, 125–43. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-24841-2_9.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
3

Rothenberg, Bat-Chen, Orna Grumberg, Yakir Vizel, and Eytan Singher. "Condition Synthesis Realizability via Constrained Horn Clauses." In Lecture Notes in Computer Science, 380–96. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-33170-1_23.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
4

Frohn, Florian, and Jürgen Giesl. "Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)." In Automated Deduction – CADE 29, 220–33. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-38499-8_13.

Повний текст джерела
Анотація:
AbstractWe recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to transition systems and introduce ADCL-NT, a variant for disproving termination. We implemented ADCL-NT in our tool and evaluate it against the state of the art.
Стилі APA, Harvard, Vancouver, ISO та ін.
5

Gurfinkel, Arie. "Program Verification with Constrained Horn Clauses (Invited Paper)." In Computer Aided Verification, 19–29. Cham: Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-13185-1_2.

Повний текст джерела
Анотація:
AbstractMany problems in program verification, Model Checking, and type inference are naturally expressed as satisfiability of a verification condition expressed in a fragment of First-Order Logic called Constrained Horn Clauses (CHC). This transforms program analysis and verification tasks to the realm of first order satisfiability and into the realm of SMT solvers. In this paper, we give a brief overview of how CHCs capture verification problems for sequential imperative programs, and discuss CHC solving algorithm underlying the Spacer engine of SMT-solver Z3.
Стилі APA, Harvard, Vancouver, ISO та ін.
6

Zavalía, Lucas, Lidiia Chernigovskaia, and Grigory Fedyukovich. "Solving Constrained Horn Clauses over Algebraic Data Types." In Lecture Notes in Computer Science, 341–65. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-24950-1_16.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
7

Unno, Hiroshi, Tachio Terauchi, and Eric Koskinen. "Constraint-Based Relational Verification." In Computer Aided Verification, 742–66. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-81685-8_35.

Повний текст джерела
Анотація:
AbstractIn recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses ($$\mathrm {CHCs}$$ CHCs ) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond k-safety such as generalized non-interference and co-termination.This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called $$\mathrm {pfwCSP}$$ pfwCSP where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over $$\mathrm {CHCs}$$ CHCs permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for $$\mathrm {pfwCSP}$$ pfwCSP based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates.We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.
Стилі APA, Harvard, Vancouver, ISO та ін.
8

Echahed, Rachid, Mnacho Echenim, Mehdi Mhalla, and Nicolas Peltier. "A Strict Constrained Superposition Calculus for Graphs." In Lecture Notes in Computer Science, 135–55. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-30829-1_7.

Повний текст джерела
Анотація:
AbstractWe propose a superposition-based proof procedure to reason on equational first order formulas defined over graphs. First, we introduce the considered graphs that are directed labeled graphs with lists of roots standing for pins or interfaces for replacements. Then the syntax and semantics of the considered logic are defined. The formulas at hand are clause sets built on equations and disequations on graphs. Afterwards, a sound and complete proof procedure is provided, and redundancy criteria are introduced to dismiss useless clauses and improve the efficiency of the procedure. In a first step, a set of inferences rules is provided in the case of uninterpreted labels. In a second step, the proposed rules are lifted to take into account labels defined as terms interpreted in some arbitrary theory. Particular formulas of interest are Horn clauses, for which stronger redundancy criteria can be devised. Essential differences with the usual term superposition calculus are emphasized.
Стилі APA, Harvard, Vancouver, ISO та ін.
9

Henn, Thomas, Marcus Völker, Stefan Kowalewski, Minh Trinh, Oliver Petrovic, and Christian Brecher. "Verification of Behavior Trees using Linear Constrained Horn Clauses." In Formal Methods for Industrial Critical Systems, 211–25. Cham: Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-15008-1_14.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
10

Blicha, Martin, Konstantin Britikov, and Natasha Sharygina. "The Golem Horn Solver." In Computer Aided Verification, 209–23. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-37703-7_10.

Повний текст джерела
Анотація:
AbstractThe logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verification of safety properties in transition systems to modular verification of programs with procedures. In this work we present Golem, a flexible and efficient solver for satisfiability of CHC over linear real and integer arithmetic. Golem provides flexibility with modular architecture and multiple back-end model-checking algorithms, as well as efficiency with tight integration with the underlying SMT solver. This paper describes the architecture of Golem and its back-end engines, which include our recently introduced model-checking algorithm TPA for deep exploration. The description is complemented by extensive evaluation, demonstrating the competitive nature of the solver.
Стилі APA, Harvard, Vancouver, ISO та ін.

Тези доповідей конференцій з теми "Constrained horn clauses"

1

Prabhu, Sumanth, Grigory Fedyukovich, Kumar Madhukar, and Deepak D'Souza. "Specification synthesis with constrained Horn clauses." In PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. New York, NY, USA: ACM, 2021. http://dx.doi.org/10.1145/3453483.3454104.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
2

Zlatkin, Ilia, and Grigory Fedyukovich. "Horntinuum: Autonomous Testing using Constrained Horn Clauses." In ASE '22: 37th IEEE/ACM International Conference on Automated Software Engineering. New York, NY, USA: ACM, 2022. http://dx.doi.org/10.1145/3551349.3563235.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
3

Fedyukovich, Grigory, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. "Solving Constrained Horn Clauses Using Syntax and Data." In 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 2018. http://dx.doi.org/10.23919/fmcad.2018.8603011.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
4

Gurfinkel, Arie, and Nikolaj Bjorner. "The Science, Art, and Magic of Constrained Horn Clauses." In 2019 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). IEEE, 2019. http://dx.doi.org/10.1109/synasc49474.2019.00010.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
5

Burn, Toby Cathcart, Luke Ong, Steven Ramsay, and Dominik Wagner. "Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses." In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2021. http://dx.doi.org/10.1109/lics52264.2021.9470527.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
6

Kafle, Bishoksan, and John P. Gallagher. "Constraint Specialisation in Horn Clause Verification." In POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, 2015. http://dx.doi.org/10.1145/2678015.2682544.

Повний текст джерела
Стилі APA, Harvard, Vancouver, ISO та ін.
Також вас можуть зацікавити розширені добірки на тему "Constrained horn clauses" для конкретних типів джерел:
Статті в журналах
Ми пропонуємо знижки на всі преміум-плани для авторів, чиї праці увійшли до тематичних добірок літератури. Зв'яжіться з нами, щоб отримати унікальний промокод!

До бібліографії