Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2012
Springer
242views Hardware» more  CAV 2012»
9 years 7 months ago
Exercises in Nonstandard Static Analysis of Hybrid Systems
Abstract. In formal verification of hybrid systems, a big challenge is to incorporate continuous flow dynamics in a discrete framework. Our previous work proposed to use nonstand...
Ichiro Hasuo, Kohei Suenaga
VMCAI
2012
Springer
10 years 29 days ago
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic. The course is ent...
Tobias Nipkow
POPL
2012
ACM
10 years 29 days ago
Probabilistic relational reasoning for differential privacy
Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential priva...
Gilles Barthe, Boris Köpf, Federico Olmedo, S...
POPL
2012
ACM
10 years 29 days ago
Syntactic control of interference for separation logic
Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one s...
Uday S. Reddy, John C. Reynolds
CSFW
2011
IEEE
10 years 5 months ago
Modular Protections against Non-control Data Attacks
—This paper introduces YARRA, a conservative extension to C to protect applications from non-control data attacks. YARRA programmers specify their data integrity requirements by ...
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swa...
ENTCS
2000
120views more  ENTCS 2000»
11 years 5 months ago
Efficient Substitution in Hoare Logic Expressions
Substitution plays an important role in Hoare Logic, as it is used in interpreting assignments. When writing a computer-based realization of Hoare Logic, it is therefore important...
Roberto Virga
EATCS
2000
108views more  EATCS 2000»
11 years 5 months ago
The Underlying Logic of Hoare Logic
Formulas of Hoare logic are asserted programs where is a program and , are assertions. The language of programs varies; in the survey [Apt 1980], one finds the language of wh...
Andreas Blass, Yuri Gurevich
ENTCS
2006
133views more  ENTCS 2006»
11 years 5 months ago
A Compositional Natural Semantics and Hoare Logic for Low-Level Languages
The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be diff...
Ando Saabas, Tarmo Uustalu
ENTCS
2006
138views more  ENTCS 2006»
11 years 5 months ago
Variables as Resource in Separation Logic
Separation logic [20,21,14] began life as an extended formalisation of Burstall's treatment of list-mutating programs [8]. It rapidly became clear that there was more that it...
Richard Bornat, Cristiano Calcagno, Hongseok Yang
ENTCS
2008
142views more  ENTCS 2008»
11 years 5 months ago
An Open System Operational Semantics for an Object-Oriented and Component-Based Language
Object orientation and component-based development have both proven useful for the elaboration of open distributed systems. These paradigms are offered by the Creol language. Creo...
Jasmin Christian Blanchette, Olaf Owe
books