uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Verifying Psi-calculi
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2010 (English)Independent thesis Advanced level (degree of Master (One Year)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Psi-calculi are mobile process calculi, parametrised with arbitrary nominal datatypes representing data, communication channels, assertions and conditions, as well as morphisms over those datatypes. The framework for psi-calculi has been formalised in the interactive theorem prover Isabelle, along with both strong and weak bisimulation.

This master's thesis project presents a tool for formally verifying that psi-calculus candidates are well-defined within the Isabelle/HOL-Nominal framework. It employs custom-made, heuristic proof tactics that discharge as many proof obligations as possible automatically, and passes any remaining proof obligations back to the user, who must supply manual proofs. The implementation of the tool as well as the proof strategies employed are described. The tool is applied to verify encodings of both the monadic and polyadic variants of the pi-calculus, as well as the pi-F calculus.

Place, publisher, year, edition, pages
2010.
Series
IT ; 10 052
Identifiers
URN: urn:nbn:se:uu:diva-132192OAI: oai:DiVA.org:uu-132192DiVA, id: diva2:357190
Uppsok
Technology
Supervisors
Examiners
Available from: 2010-10-15 Created: 2010-10-15 Last updated: 2010-10-15Bibliographically approved

Open Access in DiVA

fulltext(368 kB)269 downloads
File information
File name FULLTEXT01.pdfFile size 368 kBChecksum SHA-512
f064fc06e244d55922481fb27729cc803e8878fe69b913c4413a0714e24d2d388f5abffc812ca6e8a182179b6c63b6f142bf6821fdd120a970f7ff01a668962a
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 269 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 538 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf