Sciweavers

IACR
2011
98views more  IACR 2011»
12 years 11 months ago
New Receipt-Free E-Voting Scheme and Self-Proving Mix Net as New Paradigm
The contribution of this paper is twofold. First we present a new simple electronic voting scheme having standard re-encryption mix net back-end, which allows to cast a ballot and ...
Aram Jivanyan, Gurgen Khachatryan
TSE
2011
145views more  TSE 2011»
13 years 6 months ago
Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging
— We present an integrated method for program proving, testing, and debugging. Using the concept of metamorphic relations, we select necessary properties for target programs. For...
Tsong Yueh Chen, T. H. Tse, Zhiquan Zhou
TCS
2011
13 years 6 months ago
Correctness of linear logic proof structures is NL-complete
We provide new correctness criteria for all fragments (multiplicative, exponential, additive) of linear logic. We use these criteria for proving that deciding the correctness of a...
Paulin Jacobé de Naurois, Virgile Mogbil
IPPS
2010
IEEE
13 years 8 months ago
Runtime checking of serializability in software transactional memory
Abstract--Ensuring the correctness of complex implementations of software transactional memory (STM) is a daunting task. Attempts have been made to formally verify STMs, but these ...
Arnab Sinha, Sharad Malik
CORR
2010
Springer
96views Education» more  CORR 2010»
13 years 8 months ago
A Simple Correctness Proof for Magic Transformation
The paper presents a simple and concise proof of correctness of the magic transformation. We believe it may provide a useful example of formal reasoning about logic programs. The ...
Wlodzimierz Drabent
VLDB
2010
ACM
190views Database» more  VLDB 2010»
13 years 9 months ago
Continuous authentication on relational streams
According to the database outsourcing model, a data owner delegates database functionality to a thirdparty service provider, which answers queries received from clients. Authentic...
Stavros Papadopoulos, Yin Yang, Dimitris Papadias
CORR
2010
Springer
100views Education» more  CORR 2010»
13 years 10 months ago
A New Proof of the F5 Algorithm
The F5 algorithm is presented by Faug`ere in 2002. However, Faug`ere have not provide the rigorous proofs so far. In this paper, we will give a new complete proof and hence reveal ...
Yao Sun, Dingkang Wang
ENTCS
2008
139views more  ENTCS 2008»
13 years 11 months ago
Pervasive Compiler Verification - From Verified Programs to Verified Systems
We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pe...
Dirk Leinenbach, Elena Petrova
DSD
2007
IEEE
136views Hardware» more  DSD 2007»
13 years 11 months ago
Error-Aware Design
The universal underlying assumption made today is that Systems on chip must maintain 100% correctness regardless of the application. This work advocates the concept that some appl...
Fadi J. Kurdahi, Ahmed M. Eltawil, Amin Khajeh Dja...
ICECCS
2010
IEEE
196views Hardware» more  ICECCS 2010»
13 years 11 months ago
Implementing and Evaluating a Model Checker for Transactional Memory Systems
Abstract—Transactional Memory (TM) is a promising technique that addresses the difficulty of parallel programming. Since TM takes responsibility for all concurrency control, TM ...
Woongki Baek, Nathan Grasso Bronson, Christos Kozy...