Skapa referens, olika format (klipp och klistra)
Harvard
Johan, H. (2018) Proof Checker for Extended Linear Time Temporal Logic Proofs About Small Concurrent Programs. Göteborg : Chalmers University of Technology
BibTeX
@mastersthesis{
Johan2018,
author={Johan, Häggström},
title={Proof Checker for Extended Linear Time Temporal Logic Proofs About Small Concurrent Programs},
abstract={Program verification is a time-consuming task and prone to errors when done manually.
Verification tools are therefore essential when dealing with verification in larger
scales. As of now, most verification tools use model checking when verifying program
properties. Model checkers search for contradictions to properties regarding
those programs, and if none are found then the property is considered valid. However,
most model checkers are made for sequential programs, and with most modern
environments using concurrency, the demands on the verification tools increase accordingly.
With the success of model checking, formal proofs regarding concurrent programs
have gotten little attention the past years. Conducting formal proofs can be tedious
and error prone when done manually, but can also be very useful in terms certainty
and gaining a more intuitive understanding of the problems.
This thesis focuses on the development of a tool for formal proof checking of small
concurrent programs. The tool was developed using the functional programming
language Agda. A logic was implemented, along with a representation of a small
programming language and a proof construction system.
The final result of the project is a proof checking tool able to verify liveness proofs
regarding arbitrary programs of the specified language. The proofs are conducted
using predefined logic rules. If the proof can be implemented in the proof checker,
the proof is considered valid.
Agda turned out to be a useful tool for conducting formal proofs. The method of
formal proofs for concurrent programs is still not preferable due to the complexity
of the proofs, but with the development of more sophisticated automated theorem
provers, the method may become increasingly viable in the future.},
publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},
place={Göteborg},
year={2018},
note={56},
}
RefWorks
RT Generic
SR Electronic
ID 254939
A1 Johan, Häggström
T1 Proof Checker for Extended Linear Time Temporal Logic Proofs About Small Concurrent Programs
YR 2018
AB Program verification is a time-consuming task and prone to errors when done manually.
Verification tools are therefore essential when dealing with verification in larger
scales. As of now, most verification tools use model checking when verifying program
properties. Model checkers search for contradictions to properties regarding
those programs, and if none are found then the property is considered valid. However,
most model checkers are made for sequential programs, and with most modern
environments using concurrency, the demands on the verification tools increase accordingly.
With the success of model checking, formal proofs regarding concurrent programs
have gotten little attention the past years. Conducting formal proofs can be tedious
and error prone when done manually, but can also be very useful in terms certainty
and gaining a more intuitive understanding of the problems.
This thesis focuses on the development of a tool for formal proof checking of small
concurrent programs. The tool was developed using the functional programming
language Agda. A logic was implemented, along with a representation of a small
programming language and a proof construction system.
The final result of the project is a proof checking tool able to verify liveness proofs
regarding arbitrary programs of the specified language. The proofs are conducted
using predefined logic rules. If the proof can be implemented in the proof checker,
the proof is considered valid.
Agda turned out to be a useful tool for conducting formal proofs. The method of
formal proofs for concurrent programs is still not preferable due to the complexity
of the proofs, but with the development of more sophisticated automated theorem
provers, the method may become increasingly viable in the future.
PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,
LA eng
LK http://publications.lib.chalmers.se/records/fulltext/254939/254939.pdf
OL 30
