12 results on '"Jael Kriener"'
Search Results
2. Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics.
- Author
-
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, and Stephan Merz
- Published
- 2014
- Full Text
- View/download PDF
Catalog
3. Proofs you can believe in: proving equivalences between Prolog semantics in Coq.
- Author
-
Jael Kriener, Andy King, and Sandrine Blazy
- Published
- 2013
- Full Text
- View/download PDF
4. Mutual Exclusion by Interpolation.
- Author
-
Jael Kriener and Andy King
- Published
- 2012
- Full Text
- View/download PDF
5. Existential Quantification as Incremental SAT.
- Author
-
Jörg Brauer, Andy King, and Jael Kriener
- Published
- 2011
- Full Text
- View/download PDF
6. Correct Reasoning about Logic Programs.
- Author
-
Jael Kriener
- Published
- 2011
- Full Text
- View/download PDF
7. RedAlert: Determinacy inference for Prolog.
- Author
-
Jael Kriener and Andy King
- Published
- 2011
- Full Text
- View/download PDF
8. Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
- Author
-
Jael Kriener, Damien Doligez, Leslie Lamport, Stephan Merz, Tomer Libal, Programming languages, types, compilation and proofs (GALLIUM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Microsoft Research - Inria Joint Centre (MSR - INRIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation [Redmond, Wash.], Microsoft Research [Redmond], Microsoft Corporation [Redmond, Wash.], Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Christoph Benzmüller and Jens Otten, European Project: 295261,EC:FP7:PEOPLE,FP7-PEOPLE-2011-IRSES,MEALS(2011), Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft more...
- Subjects
FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,Normal modal logic ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,Computer Science::Logic in Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,Accessibility relation ,Mathematics ,business.industry ,Programming language ,Multimodal logic ,Modal μ-calculus ,Modal logic ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,020207 software engineering ,16. Peace & justice ,Logic in Computer Science (cs.LO) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Dynamic logic (modal logic) ,Kripke semantics ,Artificial intelligence ,T-norm fuzzy logics ,business ,computer ,Natural language processing ,Hardware_LOGICDESIGN - Abstract
We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic., Comment: appears in Automated Reasoning in Quantified Non-Classical Logics (2014) more...
- Published
- 2014
- Full Text
- View/download PDF
9. Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq
- Author
-
Andy King, Sandrine Blazy, Jael Kriener, School of Computing [Kent], University of Kent [Canterbury], Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Tom Schrijvers, LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, and Institut National de Recherche en Informatique et en Automatique (Inria) more...
- Subjects
Theoretical computer science ,Correctness ,[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] ,Semantics (computer science) ,Programming language ,Computer science ,Formal semantics (linguistics) ,Proof assistant ,computer.software_genre ,Abstract interpretation ,Operational semantics ,Well-founded semantics ,computer ,Logic programming - Abstract
International audience; Basing program analyses on formal semantics has a long and successful tradition in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and authors of such analyses often invest considerable effort into establishing these results. The development of interactive theorem provers such as Coq and their recent successes both in the field of program verification as well as in mathematics, poses the question whether these tools can be usefully deployed in logic programming. This paper presents formalisations in Coq of several general results about the correctness of semantics in different styles; forward and backward, top-down and bottom-up. The results chosen are paradigmatic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the application of interactive theorem provers to this task, as well as the difficulties likely to be encountered in the endeavour. It turns out that the advantages offered by moving to a functional setting, including the possibility to apply higher-order abstract syntax, are considerable. more...
- Published
- 2013
10. Resourceful Reachability as HORN-LA
- Author
-
Samin Ishtiaq, Jael Kriener, Josh Berdine, Christoph M. Wintersteiger, and Nikolaj Bjørner
- Subjects
Theoretical computer science ,Horn clause ,Computer science ,Reachability ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Computer Science::Logic in Computer Science ,Benchmark (computing) ,Computer Science::Programming Languages ,Context (language use) ,Solver ,Disjunctive normal form ,Symbolic execution ,Counterexample - Abstract
The program verification tool SLAyer uses abstractions during analysis and relies on a solver for reachability to refine spurious counterexamples. In this context, we extract a reachability benchmark suite and evaluate methods for encoding reachability properties with heaps using Horn clauses over linear arithmetic. The benchmarks are particularly challenging and we describe and evaluate pre-processing transformations that are shown to have significant effect. more...
- Published
- 2013
- Full Text
- View/download PDF
11. Mutual Exclusion by Interpolation
- Author
-
Andy King and Jael Kriener
- Subjects
Linear inequality ,Determinacy ,Theoretical computer science ,Control flow ,business.industry ,Computer science ,Computer programming ,Enumeration ,Mutual exclusion ,Predicate (mathematical logic) ,business ,Logic programming - Abstract
The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes. more...
- Published
- 2012
- Full Text
- View/download PDF
12. RedAlert: Determinacy Inference for Prolog
- Author
-
Andy King and Jael Kriener
- Subjects
FOS: Computer and information sciences ,Determinacy ,Computer Science - Logic in Computer Science ,Theoretical computer science ,Correctness ,Semantics (computer science) ,Computer science ,Computer programming ,Inference ,computer.software_genre ,Theoretical Computer Science ,QA76 ,Prolog ,Artificial Intelligence ,Computer Science::Logic in Computer Science ,Experimental work ,computer.programming_language ,Generality ,Computer Science - Programming Languages ,business.industry ,Programming language ,Logic in Computer Science (cs.LO) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Computational Theory and Mathematics ,Hardware and Architecture ,Computer Science::Programming Languages ,business ,computer ,Software ,Programming Languages (cs.PL) - Abstract
This paper revisits the problem of determinacy inference addressing the problem of how to uniformly handle cut. To this end a new semantics is introduced for cut, which is abstracted to systematically derive a backward analysis that derives conditions sufficient for a goal to succeed at most once. The method is conceptionally simpler and easier to implement than existing techniques, whilst improving the latter's handling of cut. Formal arguments substantiate correctness and experimental work, and a tool called 'RedAlert' demonstrates the method's generality and applicability., Theory and Practice of Logic Programming, 2011, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue, volume 11, issue 4-5 more...
- Published
- 2011
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.