History-Based Specification and Verification of Scalable Concurrent and Distributed Systems

2015 ◽  
pp. 217-233 ◽  
Author(s):  
Crystal Chang Din ◽  
S. Lizeth Tapia Tarifa ◽  
Reiner Hähnle ◽  
Einar Broch Johnsen
Keyword(s):  
Distributed Systems ◽  
Specification And Verification ◽  
Concurrent And Distributed Systems

scholarly journals Gobra: Modular Specification and Verification of Go Programs

2021 ◽  
pp. 367-379
Author(s):  
Felix A. Wolf ◽  
Linard Arquint ◽  
Martin Clochard ◽  
Wytse Oortwijn ◽  
João C. Pereira ◽  
...  
Keyword(s):  
Distributed Systems ◽  
Programming Language ◽  
Message Passing ◽  
Safety Data ◽  
Separation Logic ◽  
Data Race ◽  
Static Verification ◽  
Crash Safety ◽  
Concurrent And Distributed Systems ◽  
Systems Programming

AbstractGo is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives.We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.

Sign in / Sign up

Export Citation Format

Share Document