Over the last forty years, computer scientists have invented or borrowed numerous logics for reasoning about digital systems. Here, I would like to concentrate on three of them: Linear Time Temporal logic (LTL), branc...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Over the last forty years, computer scientists have invented or borrowed numerous logics for reasoning about digital systems. Here, I would like to concentrate on three of them: Linear Time Temporal logic (LTL), branching time Computation Tree temporal logic (CTL), and Propositional Dynamic logic (PDL), with and without converse. More specifically, I would like to present results and techniques on how to solve the satisfiability problem in these logics, with global assumptions, using the tableau method. the issues that arise are the typical tensions between computational complexity, practicality and scalability. this is joint work with Linh Anh Nguyen, Pietro Abate, Linda Postniece, Florian Widmann and Jimmy thomson.
Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program and that can be used to prove memory safety. this graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.
MleanCoP is a fully automatedtheorem prover for first-order modal logic. the proof search is based on a prefixed connection calculus and an additional prefix unification, which captures the Kripke semantics of differ...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
MleanCoP is a fully automatedtheorem prover for first-order modal logic. the proof search is based on a prefixed connection calculus and an additional prefix unification, which captures the Kripke semantics of different modal logics. MleanCoP is implemented in Prolog and the source code of the core proof search procedure consists only of a few lines. It supports the standard modal logics D, T, S4, and S5 with constant, cumulative, and varying domain conditions. the most recent version also supports heterogeneous multimodal logics and outputs a compact prefixed connection proof. An experimental evaluation shows the strong performance of MleanCoP.
We present a focused intuitionistic sequent calculus for higher-order logic. It has primitive support for equality and mixes.-term conversion with equality reasoning. Classical reasoning is enabled by extending the sy...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We present a focused intuitionistic sequent calculus for higher-order logic. It has primitive support for equality and mixes.-term conversion with equality reasoning. Classical reasoning is enabled by extending the system with rules for reductio ad absurdum and the axiom of choice. the resulting system is proved sound with respect to Church's simple type theory. the soundness proof has been formalized in Agda. A theorem prover based on bottom-up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. the problems for which the theorem prover performs best require higher-order unification more frequently than the average higher-order TPTP problem. Being strong at higher-order unification, the system may serve as a complement to other theorem provers in the field.
the differential temporal dynamic logic dTL(2) is a logic to specify temporal properties of hybrid systems. It combines differential dynamic logic with temporal logic to reason about the intermediate states reached by...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
the differential temporal dynamic logic dTL(2) is a logic to specify temporal properties of hybrid systems. It combines differential dynamic logic with temporal logic to reason about the intermediate states reached by a hybrid system. the logic dTL(2) supports some linear time temporal properties of LTL. It extends differential temporal dynamic logic dTL with nested temporalities. We provide a semantics and a proof system for the logic dTL(2), and show its usefulness for nontrivial temporal properties of hybrid systems. We take particular care to handle the case of alternating universal dynamic and existential temporal modalities and its dual, solving an open problem formulated in previous work.
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form for all x.A (for quantifier-...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form for all x.A (for quantifier-free A) to a method generating lemmas of the form for all x(1) ... for all x(n).A. Moreover, we extend the original method to predicate logic with equality. the new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.
We introduce a robust and tractable temporal logic, we call Visibly Linear Temporal logic (VLTL), which captures the full class of Visibly Pushdown Languages. the novel logic avoids fix points and provides instead nat...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We introduce a robust and tractable temporal logic, we call Visibly Linear Temporal logic (VLTL), which captures the full class of Visibly Pushdown Languages. the novel logic avoids fix points and provides instead natural temporal operators with simple and intuitive semantics. We prove that the complexities of the satisfiability and visibly pushdown model checking problems are the same as for other well known logics, like CaRet and the nested word temporal logic NWTL, which in contrast are strictly more limited in expressive power than VLTL. Moreover, formulas of CaRet and NWTL can be easily and inductively translated in linear-time into VLTL.
We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL(+) of the full Alternating time temporal logic ...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL(+) of the full Alternating time temporal logic ATL*. the method extends in an essential way a previously developed tableaux-based decision method for ATL and works in 2EXP-TIME, which is the optimal worst case complexity of the satisfiability problem for ATL(+). We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL(+) formulae can reduce the complexity of the satisfiability problem.
We introduce StarExec, a public web-based service built to facilitate the experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning. Examples of such tools include theor...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We introduce StarExec, a public web-based service built to facilitate the experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning. Examples of such tools include theorem provers, SAT and SMT solvers, constraint solvers, model checkers, and software verifiers. the service, running on a compute cluster with 380 processors and 23 terabytes of disk space, is designed to provide a single piece of storage and computing infrastructure to logic solving communities and their members. It aims at reducing duplication of effort and resources as well as enabling individual researchers or groups with no access to comparable infrastructure. StarExec allows community organizers to store, manage and make available benchmark libraries;competition organizers to run logic solver competitions;and community members to do comparative evaluations of logic solvers on public or private benchmark problems.
Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more tradi...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures. After an introduction to electronic voting, we describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.
暂无评论