Sciweavers

PODS
2010
ACM
197views Database» more  PODS 2010»
14 years 20 days ago
When data dependencies over SQL tables meet the logics of paradox and S-3
We study functional and multivalued dependencies over SQL tables with NOT NULL constraints. Under a no-information interpretation of null values we develop tools for reasoning. We...
Sven Hartmann, Sebastian Link
CAV
2010
Springer
286views Hardware» more  CAV 2010»
14 years 20 days ago
ABC: An Academic Industrial-Strength Verification Tool
ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transforma...
Robert K. Brayton, Alan Mishchenko
APLAS
2010
ACM
14 years 21 days ago
Reasoning about Computations Using Two-Levels of Logic
We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the "reasoning logic", is used to state th...
Dale Miller
ECOOP
2008
Springer
14 years 1 months ago
Regional Logic for Local Reasoning about Global Invariants
Shared mutable objects pose grave challenges in reasoning, especially for data abstraction and modularity. This paper presents a novel logic for erroravoiding partial correctness o...
Anindya Banerjee, David A. Naumann, Stan Rosenberg
CSL
2010
Springer
14 years 1 months ago
Automata vs. Logics on Data Words
Abstract. The relationship between automata and logics has been investigated since the 1960s. In particular, it was shown how to determine, given an automaton, whether or not it is...
Michael Benedikt, Clemens Ley, Gabriele Puppis
CSL
2010
Springer
14 years 1 months ago
Ordered Sets in the Calculus of Data Structures
Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints...
Viktor Kuncak, Ruzica Piskac, Philippe Suter
ASIAN
2009
Springer
363views Algorithms» more  ASIAN 2009»
14 years 1 months ago
A Logic for Formal Verification of Quantum Programs
Abstract. This paper provides a Hoare-style logic for quantum computation. While the usual Hoare logic helps us to verify classical deterministic programs, our logic supports quant...
Yoshihiko Kakutani
ISMB
1994
14 years 1 months ago
Using Interval Logic for Order Assembly
Temporallogic, in particular, interval logic has been used to represent genomemapsand to assist genome mapconstructions. However,interval logic itself appears to be bruited in its...
Zhan Cui
AAAI
2000
14 years 1 months ago
A Flexible Framework for Defeasible Logics
Logics for knowledge representation suffer from overspecialization: while each logic may provide an ideal representation formalism for some problems, it is less than optimal for o...
Grigoris Antoniou, David Billington, Guido Governa...
IWFM
2003
123views Formal Methods» more  IWFM 2003»
14 years 1 months ago
Logic for Computational Effects: Work in Progress
We outline a possible logic that will allow us to give a unified approach to reasoning about computational effects. The logic is given by extending Moggi’s computational λ-cal...
Gordon D. Plotkin, John Power