Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAlethe: Towards a Generic SMT Proof Format (extended abstract)
70
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format.
rate research
Read More
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coqs automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.
While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the emphasis of model checking is on establishing the truth of a property in a model, we rely on the proof theoretic notion of additive inference rules, since such rules allow provability to directly describe truth conditions. Unfortunately, the additive treatment of quantifiers requires inference rules to have infinite sets of premises and the additive treatment of model descriptions provides no natural notion of state exploration. By employing a focused proof system, it is possible to construct large scale, synthetic rules that also qualify as additive but contain elements of multiplicative inference. These additive synthetic rules -- essentially rules built from the description of a model -- allow a direct treatment of state exploration. This proof theoretic framework provides a natural treatment of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.
Process behaviour is often defined either in terms of the tests they satisfy, or in terms of the logical properties they enjoy. Here we compare these two approaches, using extensional testing in the style of DeNicola, Hennessy, and a recursive version of the property logic HML. We first characterise subsets of this property logic which can be captured by tests. Then we show that those subsets of the property logic capture precisely the power of tests.
This is an extended abstract presenting new results on the topological complexity of omega-powers (which are included in a paper Classical and effective descriptive complexities of omega-powers available from arXiv:0708.4176) and reflecting also some open questions which were discussed during the Dagstuhl seminar on Topological and Game-Theoretic Aspects of Infinite Computations 29.06.08 - 04.07.08.
RNA interference (RNAi) is a mechanism whereby small RNAs (siRNAs) directly control gene expression without assistance from proteins. This mechanism consists of interactions between RNAs and small RNAs both of which may be single or double stranded. The target of the mechanism is mRNA to be degraded or aberrated, while the initiator is double stranded RNA (dsRNA) to be cleaved into siRNAs. Observing the digital nature of RNAi, we represent RNAi as a Minsky register machine such that (i) The two registers hold single and double stranded RNAs respectively, and (ii) Machines instructions are interpreted by interactions of enzyme (Dicer), siRNA (with RISC com- plex) and polymerization (RdRp) to the appropriate registers. Interpreting RNAi as a computational structure, we can investigate the computational meaning of RNAi, especially its complexity. Initially, the machine is configured as a Chemical Ground Form (CGF), which generates incorrect jumps. To remedy this problem, the system is remodeled as recursive RNAi, in which siRNA targets not only mRNA but also the machine instructional analogues of Dicer and RISC. Finally, probabilistic termination is investigated in the recursive RNAi system.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
