Zaloguj się

Gotowe bibliografie tematyczne / Constrained horn clauses

Spis treści

Artykuły w czasopismach
Rozprawy doktorskie
Części książek
Streszczenia konferencji

Gotowa bibliografia na temat „Constrained horn clauses”

Autor: Grafiati

Data publikacji: 6 września 2023

Utwórz poprawne odniesienie w stylach APA, MLA, Chicago, Harvard i wielu innych

Wybierz rodzaj źródła:

Zobacz listy aktualnych artykułów, książek, rozpraw, streszczeń i innych źródeł naukowych na temat „Constrained horn clauses”.

Przycisk „Dodaj do bibliografii” jest dostępny obok każdej pracy w bibliografii. Użyj go – a my automatycznie utworzymy odniesienie bibliograficzne do wybranej pracy w stylu cytowania, którego potrzebujesz: APA, MLA, Harvard, Chicago, Vancouver itp.

Możesz również pobrać pełny tekst publikacji naukowej w formacie „.pdf” i przeczytać adnotację do pracy online, jeśli odpowiednie parametry są dostępne w metadanych.

Artykuły w czasopismach na temat "Constrained horn clauses"

1

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

2

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

3

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

4

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

5

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

6

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

7

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

8

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

9

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

10

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

Więcej źródeł

Rozprawy doktorskie na temat "Constrained horn clauses"

1

Reuß, Andreas [Verfasser], Helmut [Akademischer Betreuer] Seidl i 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.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

2

Reuß, Andreas Verfasser], Helmut [Akademischer Betreuer] [Seidl i 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.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Części książek na temat "Constrained horn clauses"

1

Zlatkin, Ilia, i Grigory Fedyukovich. "Maximizing Branch Coverage with Constrained Horn Clauses". W 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.

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

2

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

3

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

4

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

5

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

6

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

7

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

8

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

9

Henn, Thomas, Marcus Völker, Stefan Kowalewski, Minh Trinh, Oliver Petrovic i Christian Brecher. "Verification of Behavior Trees using Linear Constrained Horn Clauses". W 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.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

10

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

Pełny tekst źródła

Streszczenie:

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.

Style APA, Harvard, Vancouver, ISO itp.

Streszczenia konferencji na temat "Constrained horn clauses"

1

Prabhu, Sumanth, Grigory Fedyukovich, Kumar Madhukar i Deepak D'Souza. "Specification synthesis with constrained Horn clauses". W 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.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

2

Zlatkin, Ilia, i Grigory Fedyukovich. "Horntinuum: Autonomous Testing using Constrained Horn Clauses". W 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.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

3

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

4

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

5

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

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

6

Kafle, Bishoksan, i John P. Gallagher. "Constraint Specialisation in Horn Clause Verification". W 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.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Oferujemy zniżki na wszystkie plany premium dla autorów, których prace zostały uwzględnione w tematycznych zestawieniach literatury. Skontaktuj się z nami, aby uzyskać unikalny kod promocyjny!