相关论文: Encapsulation for Practical Simplification Procedu…
2LS is a framework for analysis of sequential C programs that can verify and refute program assertions and termination. The 2LS framework is built upon the CPROVER infrastructure and implements template-based synthesis techniques, e.g. to…
This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined…
We give new proofs of soundness (all representable functions on base types lies in certain complexity classes) for Elementary Affine Logic, LFPL (a language for polytime computation close to realistic functional programming introduced by…
Precisely modeling complex systems like cyber-physical systems is challenging, which often render model-based system verification techniques like model checking infeasible. To overcome this challenge, we propose a method called LAR to…
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a…
We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which…
Answer set programming is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing different knowledge representation formalisms. Frequently, several related and yet substantially…
SOFT ('Second-Order Functions and Theorems') is a tool to mimic second-order functions and theorems in the first-order logic of ACL2. Second-order functions are mimicked by first-order functions that reference explicitly designated…
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of…
We investigate the interplay between a modality for controlling the behaviour of recursive functional programs on infinite structures which are completely silent in the syntax. The latter means that programs do not contain "marks" showing…
We introduce a framework for reasoning about the security of computer systems using modal logic. This framework is sufficiently expressive to capture a variety of known security properties, while also being intuitive and independent of…
Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC)…
In synchronous rewriting, the productions of two rewriting systems are paired and applied synchronously in the derivation of a pair of strings. We present a new synchronous rewriting system and argue that it can handle certain phenomena…
We consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear…
Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we…
And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence…
By any account, the 1998 proof of the Kepler conjecture is complex. The thesis underlying this article is that the proof is complex because it is highly under-automated. Throughout that proof, manual procedures are used where automated ones…
In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystems whose top-level assurance relies on the assurance of the…
From a long time ago, beside encryption of data and making it secure, compression packing it was also important that could make transmission of data faster. In the past years need for improvement of encryption and compression for a fast and…
Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field; they are used to encode computations in cryptographic zero-knowledge proofs. We make the following contributions to the…