Relevant bibliographies by topics / Craig Interpolants

Academic literature on the topic 'Craig Interpolants'

Author: Grafiati
Published: 14 March 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Contents

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Craig Interpolants.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "Craig Interpolants"

1

Artale, Alessandro, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter. "Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions." Proceedings of the AAAI Conference on Artificial Intelligence 35, no. 7 (May 18, 2021): 6193–201. http://dx.doi.org/10.1609/aaai.v35i7.16770.

Full text
Abstract:
The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit definability is valid. Thus, the CIP and PBDP transform potentially hard existence problems into deduction problems in the underlying logic. Description Logics with nominals and/or role inclusions do not enjoy the CIP nor PBDP, but interpolants and explicit definitions have many potential applications in ontology engineering and ontology-based data management. In this article we show the following: even without Craig and Beth, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as ALCO, ALCH and ALCHIO. However, living without Craig and Beth makes this problem harder than deduction: we prove that the existence problems become 2EXPTIME-complete, thus one exponential harder than validity. The existence of explicit definitions is 2EXPTIME-hard even if one asks for a definition of a nominal using any symbol distinct from that nominal, but it becomes EXPTIME-complete if one asks for a definition of a concept name using any symbol distinct from that concept name.
APA, Harvard, Vancouver, ISO, and other styles
2

Cimatti, Alessandro, Alberto Griggio, and Roberto Sebastiani. "Efficient generation of craig interpolants in satisfiability modulo theories." ACM Transactions on Computational Logic 12, no. 1 (October 2010): 1–54. http://dx.doi.org/10.1145/1838552.1838559.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Cabodi, Gianpiero, Carmelo Loiacono, and Danilo Vendraminetto. "Optimization techniques for craig interpolant compaction in unbounded model checking." Formal Methods in System Design 46, no. 2 (April 2015): 135–62. http://dx.doi.org/10.1007/s10703-015-0229-0.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

OLKHOVIKOV, GRIGORY K. "RESTRICTED INTERPOLATION AND LACK THEREOF IN STIT LOGIC." Review of Symbolic Logic 13, no. 3 (September 13, 2019): 459–82. http://dx.doi.org/10.1017/s1755020319000406.

Full text
Abstract:
AbstractWe consider the propositional logic equipped with Chellas stit operators for a finite set of individual agents plus the historical necessity modality. We settle the question of whether such a logic enjoys restricted interpolation property, which requires the existence of an interpolant only in cases where the consequence contains no Chellas stit operators occurring in the premise. We show that if action operators count as logical symbols, then such a logic has restricted interpolation property iff the number of agents does not exceed three. On the other hand, if action operators are considered to be nonlogical symbols, then the restricted interpolation fails for any number of agents exceeding one. It follows that unrestricted Craig interpolation also fails for almost all versions of stit logic.
APA, Harvard, Vancouver, ISO, and other styles
5

Krajíček, Jan. "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic." Journal of Symbolic Logic 62, no. 2 (June 1997): 457–86. http://dx.doi.org/10.2307/2275541.

Full text
Abstract:
AbstractA proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1)Feasible interpolation theorems for the following proof systems:(a)resolution(b)a subsystem of LK corresponding to the bounded arithmetic theory (α)(c)linear equational calculus(d)cutting planes.(2)New proofs of the exponential lower bounds (for new formulas)(a)for resolution ([15])(b)for the cutting planes proof system with coefficients written in unary ([4]).(3)An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory (α).In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle.
APA, Harvard, Vancouver, ISO, and other styles
6

Blicha, Martin, Antti E. J. Hyvärinen, Jan Kofroň, and Natasha Sharygina. "Using linear algebra in decomposition of Farkas interpolants." International Journal on Software Tools for Technology Transfer, August 5, 2021. http://dx.doi.org/10.1007/s10009-021-00641-z.

Full text
Abstract:
AbstractThe use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas’ lemma. However, these interpolants do not always suit the verification task—in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.
APA, Harvard, Vancouver, ISO, and other styles
7

Backeman, Peter, Philipp Rümmer, and Aleksandar Zeljić. "Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic." Formal Methods in System Design, May 12, 2021. http://dx.doi.org/10.1007/s10703-021-00372-6.

Full text
Abstract:
AbstractThe inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bit-vector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.
APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic "Craig Interpolants"

1

Weissenbacher, Georg. "Program analysis with interpolants." Thesis, University of Oxford, 2010. http://ora.ox.ac.uk/objects/uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6.

Full text
Abstract:
This dissertation discusses novel techniques for interpolation-based software model checking, an approximate method which uses Craig interpolation to compute invariants of programs. Our work addresses two aspects of program analyses based on model checking: verification (the construction of correctness proofs for programs) and falsification (the detection of counterexamples that violate the specification). In Hoare's calculus, a proof of correctness comprises assertions which establish that a program adheres to its specification. The principal challenge is to derive appropriate assertions and loop invariants. Contemporary software verification tools use Craig interpolation (as opposed to traditional predicate transformers such as the weakest precondition) to derive approximate assertions. The performance of the model checker is contingent on the Craig interpolants computed. We present novel interpolation techniques which provide the following advantages over existing methods. Firstly, the resulting interpolants are sound with respect to the bit-level semantics of programs, which is an improvement over interpolation systems that use linear arithmetic over the reals to approximate bit-vector arithmetic and/or do not support bit-level operations. Secondly, our interpolation systems afford us a choice of interpolants and enable us to fine-tune their logical strength and structure. In contrast, existing procedures are limited to a single ad-hoc choice of an interpolant. Interpolation-based verification tools are typically forced to refine an initial approximation repeatedly in order to achieve the accuracy required to establish or refute the correctness of a program. The detection of a counterexample containing a repetitive construct may necessitate one refinement step (involving the computation of additional interpolants) for each iteration of the loop. We present a heuristic that aims to avoid the repeated and computationally expensive construction of interpolants, thus enabling the detection of deeply buried defects such as buffer overflows. Finally, we present an implementation of our techniques and evaluate them on a set of standardised device driver and buffer overflow benchmarks.
APA, Harvard, Vancouver, ISO, and other styles
2

Blicha, Martin. "Metody pro redukci velikosti interpolantů při použití částečného přiřazení." Master's thesis, 2016. http://www.nusl.cz/ntk/nusl-352598.

Full text
Abstract:
Abstract. Since the introduction of interpolants to the field of symbolic model checking, interpolation-based methods have been successfully used in both hardware and software model checking. Recently, variable assignments have been introduced to the computation of interpolants. In the context of abstract reachability graphs, variable assignment can be used not only to prevent out-of-scope variables from appearing in interpolants, but also to reduce the size of the interpolant significantly. We further extend the framework for computing interpolants under variable assignment, prove the correctness of the system and show that it has potential to further decrease the size of the computed interpolants. At the end we analyze under which conditions the computed interpolants will still have the path interpolation property, a desired property in many interpolation-based techniques. 1
APA, Harvard, Vancouver, ISO, and other styles
3

Jančík, Pavel. "Reprezentace stavů programu." Doctoral thesis, 2017. http://www.nusl.cz/ntk/nusl-369534.

Full text
Abstract:
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
APA, Harvard, Vancouver, ISO, and other styles

Book chapters on the topic "Craig Interpolants"

1

Schöning, Uwe, and Randall Pruim. "The Complexity of Craig Interpolants." In Gems of Theoretical Computer Science, 111–13. Berlin, Heidelberg: Springer Berlin Heidelberg, 1998. http://dx.doi.org/10.1007/978-3-642-60322-8_14.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

McMillan, K. L. "Applications of Craig Interpolants in Model Checking." In Tools and Algorithms for the Construction and Analysis of Systems, 1–12. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/978-3-540-31980-1_1.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Gupta, Utkarsh, Irina Ilioaea, Vikas Rao, Arpitha Srinath, Priyank Kalla, and Florian Enescu. "Rectification of Arithmetic Circuits with Craig Interpolants in Finite Fields." In VLSI-SoC: Design and Engineering of Electronics Systems Based on New Computing Paradigms, 79–106. Cham: Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-23425-6_5.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

Miller, Christian, Stefan Kupferschmid, Matthew Lewis, and Bernd Becker. "Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs." In Theory and Applications of Satisfiability Testing – SAT 2010, 194–208. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. http://dx.doi.org/10.1007/978-3-642-14186-7_17.

Full text
APA, Harvard, Vancouver, ISO, and other styles
5

Gan, Ting, Bican Xia, Bai Xue, Naijun Zhan, and Liyun Dai. "Nonlinear Craig Interpolant Generation." In Computer Aided Verification, 415–38. Cham: Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-53288-8_20.

Full text
APA, Harvard, Vancouver, ISO, and other styles

Conference papers on the topic "Craig Interpolants"

1

Gupta, Utkarsh, Irina Ilioaea, Vikas Rao, Arpitha Srinath, Priyank Kalla, and Florian Enescu. "On the Rectifiability of Arithmetic Circuits using Craig Interpolants in Finite Fields." In 2018 IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC). IEEE, 2018. http://dx.doi.org/10.1109/vlsi-soc.2018.8644853.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Jung, Jean Christoph, and Frank Wolter. "Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments." In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2021. http://dx.doi.org/10.1109/lics52264.2021.9470585.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Fortin, Marie, Boris Konev, and Frank Wolter. "Interpolants and Explicit Definitions in Extensions of the Description Logic EL." In 19th International Conference on Principles of Knowledge Representation and Reasoning {KR-2022}. California: International Joint Conferences on Artificial Intelligence Organization, 2022. http://dx.doi.org/10.24963/kr.2022/16.

Full text
Abstract:
We show that the vast majority of extensions of the description logic EL do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for EL with nominals, EL with the universal role, EL with role hierarchies and transitive roles, and for ELI. It follows in particular that the existence of an explicit definition of a concept or individual name cannot be reduced to subsumption checking via implicit definability. We show that nevertheless the existence of interpolants and explicit definitions can be decided in polynomial time for standard tractable extensions of EL (such as EL++) and in ExpTime for ELI and various extensions. It follows that these existence problems are not harder than subsumption which is in sharp contrast to the situation for expressive DLs. We also obtain tight bounds for the size of interpolants and explicit definitions and the complexity of computing them: single exponential for tractable standard extensions of EL and double exponential for ELI and extensions. We close with a discussion of Horn-DLs such as Horn-ALCI.
APA, Harvard, Vancouver, ISO, and other styles
4

Jung, Jean Christoph, Carsten Lutz, Hadrien Pulcini, and Frank Wolter. "Separating Data Examples by Description Logic Concepts with Restricted Signatures." In 18th International Conference on Principles of Knowledge Representation and Reasoning {KR-2021}. California: International Joint Conferences on Artificial Intelligence Organization, 2021. http://dx.doi.org/10.24963/kr.2021/37.

Full text
Abstract:
We study the separation of positive and negative data examples in terms of description logic concepts in the presence of an ontology. In contrast to previous work, we add a signature that specifies a subset of the symbols that can be used for separation, and we admit individual names in that signature. We consider weak and strong versions of the resulting problem that differ in how the negative examples are treated and we distinguish between separation with and without helper symbols. Within this framework, we compare the separating power of different languages and investigate the complexity of deciding separability. While weak separability is shown to be closely related to conservative extensions, strongly separating concepts coincide with Craig interpolants, for suitably defined encodings of the data and ontology. This enables us to transfer known results from those fields to separability. Conversely, we obtain original results on separability that can be transferred backward. For example, rather surprisingly, conservative extensions and weak separability in ALCO are both 3ExpTime-complete.
APA, Harvard, Vancouver, ISO, and other styles
5

Cabodi, G., C. Loiacono, and D. Vendraminetto. "Optimization Techniques for Craig Interpolant Compaction in Unbounded Model Checking." In Design Automation and Test in Europe. New Jersey: IEEE Conference Publications, 2013. http://dx.doi.org/10.7873/date.2013.289.

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

Lin, Wang, Mi Ding, Kaipeng Lin, Guoquan Mei, and Zuohua Ding. "Formal Synthesis of Neural Craig Interpolant via Counterexample Guided Deep Learning." In 2022 9th International Conference on Dependable Systems and Their Applications (DSA). IEEE, 2022. http://dx.doi.org/10.1109/dsa56465.2022.00023.

Full text
APA, Harvard, Vancouver, ISO, and other styles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography