FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
CAV ON FRIDAY, JULY 13TH
Days:
next day
all days

View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 83C: CAV Tutorial: Shaz Qadeer (part 1)
Location: Maths LT3
09:00
Proving a concurrent program correct by demonstrating it does nothing
SPEAKER: Shaz Qadeer

ABSTRACT. CIVL is a verifier for concurrent programs implemented as a conservative extension to the Boogie verification system. CIVL allows the proof of correctness of a concurrent program —shared-memory or message-passing— to be described as a sequence of program layers. The safety of a layer implies the safety of the layer just below, thus allowing the safety of the highest layer to transitively imply the safety of the lowest.

The central theme in CIVL is reasoning about atomic actions. Different layers of a program describe its behavior using atomic actions, higher layers with coarse-grained and lower layers with fine-grained atomic actions. A proof of correctness amounts to a demonstration that the highest layer is SKIP, the atomic action that does nothing. The formal and automated verification justifying the connection between adjacent layers combines several techniques—linear variables, reduction based on movers, location invariants, and procedure-local abstraction.

CIVL is available in the master branch of Boogie together with more than fifty micro-benchmarks. CIVL has also been used to refine a realistic concurrent garbage-collection algorithm from a simple high-level specification down to a highly-concurrent implementation described in terms of individual memory accesses.

10:30-11:00Coffee Break
11:00-12:30 Session 86B: CAV Tutorial: Shaz Qadeer (part 2)
Location: Maths LT3
11:00
Proving a concurrent program correct by demonstrating it does nothing (continued)
SPEAKER: Shaz Qadeer

ABSTRACT. CIVL is a verifier for concurrent programs implemented as a conservative extension to the Boogie verification system. CIVL allows the proof of correctness of a concurrent program —shared-memory or message-passing— to be described as a sequence of program layers. The safety of a layer implies the safety of the layer just below, thus allowing the safety of the highest layer to transitively imply the safety of the lowest.

The central theme in CIVL is reasoning about atomic actions. Different layers of a program describe its behavior using atomic actions, higher layers with coarse-grained and lower layers with fine-grained atomic actions. A proof of correctness amounts to a demonstration that the highest layer is SKIP, the atomic action that does nothing. The formal and automated verification justifying the connection between adjacent layers combines several techniques—linear variables, reduction based on movers, location invariants, and procedure-local abstraction.

CIVL is available in the master branch of Boogie together with more than fifty micro-benchmarks. CIVL has also been used to refine a realistic concurrent garbage-collection algorithm from a simple high-level specification down to a highly-concurrent implementation described in terms of individual memory accesses.

12:30-14:00Lunch Break
14:00-15:30 Session 87C: CAV Tutorial: Matteo Maffei
Location: Maths LT3
14:00
Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
SPEAKER: Matteo Maffei

ABSTRACT. The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics.

This tutorial will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust, a framework for the static analysis of Ethereum smart contracts that we recently introduced, which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first static analysis for EVM bytecode that comes with a proof of soundness.

15:30-16:00Coffee Break
16:30-18:00 Session 90: Talks in memoriam Mike Gordon
Location: Maths LT3
16:30
Proof Scripting from HOL to Goaled
17:00
HOL Developed and HOL Used: Interconnected Stories of Real-World Applications

ABSTRACT. I will describe work, starting with my PhD, that involved use of the HOL system’s evolving capabilities to model and verify properties of detailed real-world systems. In particular, HOL turns out to be a great tool for operational semantics applications. The projects I worked on in Cambridge were formalisations of C and TCP/IP, and both point forward to more recent work of the 2010s. At the same time, I will try to describe the work I and others put into making HOL an ever-more capable system for supporting such work.

 

17:30
From Processor Verification Upwards
19:00-21:30 Workshops dinner at Keble College

Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).

Location: Keble College