Search results: Found 4

Listing 1 - 4 of 4
Sort by
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler

Author:
ISBN: 9783866448858 Year: Pages: XXI, 412 p. DOI: 10.5445/KSP/1000028867 Language: ENGLISH
Publisher: KIT Scientific Publishing
Subject: Computer Science
Added to DOAB on : 2019-07-30 20:01:59
License:

Loading...
Export citation

Choose an application

Abstract

The Java programming language provides safety and security guarantees such as type safety and its security architecture. They distinguish it from other mainstream programming languages like C and C++. In this work, we develop a machine-checked model of concurrent Java and the Java memory model and investigate the impact of concurrency on these guarantees. From the formal model, we automatically obtain an executable verified compiler to bytecode and a validated virtual machine.

From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security

Author:
ISBN: 9783866445949 Year: Pages: XIX, 203 p. DOI: 10.5445/KSP/1000020678 Language: ENGLISH
Publisher: KIT Scientific Publishing
Subject: Computer Science
Added to DOAB on : 2019-07-30 20:02:00
License:

Loading...
Export citation

Choose an application

Abstract

This book presents a modular framework for slicing in the proof assistant Isabelle/HOL which is based on abstract control flow graphs. Building on such abstract structures renders the correctness results language-independent. To prove that they hold for a specific language, it remains to instantiate the framework with this language, which requires a formal semantics of this language in Isabelle/HOL. We show that formal semantics even for sophisticated high-level languages are realizable.

Lazy Evaluation: From natural semantics to a machine-checked compiler transformation

Author:
ISBN: 9783731505464 Year: Pages: XIV, 231 p. DOI: 10.5445/KSP/1000056002 Language: ENGLISH
Publisher: KIT Scientific Publishing
Subject: Computer Science
Added to DOAB on : 2019-07-30 20:01:57
License:

Loading...
Export citation

Choose an application

Abstract

In order to solve a long-standing problem with list fusion, a new compiler transformation, “Call Arity” is developed and implemented in the Haskell compiler GHC. It is formally proven to not degrade program performance; the proof is machine-checked using the interactive theorem prover Isabelle. To that end, a formalization of Launchbury’s Natural Semantics for Lazy Evaluation is modelled in Isabelle, including a correctness and adequacy proof.

Specification and verification of object-oriented software components

Author:
ISBN: 3866440421 Year: Pages: XVIII, 248 p. DOI: 10.5445/KSP/1000004542 Language: GERMAN
Publisher: KIT Scientific Publishing
Subject: Computer Science
Added to DOAB on : 2019-07-30 20:01:58
License:

Loading...
Export citation

Choose an application

Abstract

This work presents a flexible methodology for formally specifying and deductively verifying object-oriented components.It is based on a simple notion of program correctness. Correctness can be achieved with a novel system of proof obligations, which serve as input to a suitable theorem prover.

Listing 1 - 4 of 4
Sort by
Narrow your search

Publisher

KIT Scientific Publishing (4)


License

CC by-nc-nd (3)

CC by-sa (1)


Language

english (3)

german (1)


Year
From To Submit

2016 (1)

2012 (1)

2011 (1)

2006 (1)