Titlebook: Software Engineering and Formal Methods; 13th International C Radu Calinescu,Bernhard Rumpe Conference proceedings 2015 Springer Internatio

Arable

翻动

禁令

Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specificationmalized in VeriFast, a separation logic-based verifier for C programs. By giving formal contracts to the primitives of an existing cryptographic library (i.e. PolarSSL), we were able to prove, besides memory safety, interesting security properties of a small protocol suite thatdemonstrates the usage of those primitives.

Memorial

Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioningnformation only if it cannot easily be recomputed. The second approach partitions the certificate into independently checkable parts. The trick is to read parts of the certificate while already checking read parts. Our experiments show that validation highly benefits from our improvements.

Humble

Deduct

THE

An Interface Theory for the Internet of Things, it examines an architecture for IoT applications where so-called “accessors” provide an actor-oriented proxy for devices (“things”) and services. Following the principles of actor models, an accessor reacts to input stimuli and produces outputs that can stimulate reactions in other accessors or ac

抗体

Learning Assertions to Verify Linked-List Programs analysis of dsOli to locate and identify data structure operations in a program, and then use this information to automatically annotate that program with assertions in separation logic. These annotations comprise candidate pre/post-conditions and loop invariants suitable to statically verify memor

Hyperplasia

表状态

Specification and Verification of Atomic Operations in GPGPU Programsrnels that use . as synchronisation mechanism. Our approach exploits the notion of . from Concurrent Separation Logic (CSL) to capture the behaviour of atomic operations. However, because of the different memory levels in the GPU architecture, we adapt this notion of resource invariant to these memo