Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • 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
Machine Assisted Reasoning for Multi-Threaded Java Bytecode
KTH, School of Information and Communication Technology (ICT), Electronic, Computer and Software Systems, ECS.
2005 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Datorstödda resonemang om multi-trådad Java-bytekod (Swedish)
Abstract [en]

In this thesis an operational semantics for a subset of the Java Virtual Machine (JVM) is developed and presented. The subset contains standard operations such as control flow, computation, and memory management. In addition, the subset contains a treatment of parallel threads of execution. The operational semantics are embedded into a $µ$-calculus based proof assistant, called the VeriCode Proof Tool (VCPT). VCPT has been developed at the Swedish Institute of Computer Science (SICS), and has powerful features for proving inductive assertions. Some examples of proving properties of programs using the embedding are presented.

 

Abstract [sv]

I det här examensarbetet  presenteras en operationell semantik för en delmängd av Javas virtuella maskin. Den delmängd som hanteras innehåller kontrollflöde, beräkningar och minneshantering. Vidare beskrivs  semantiken för parallella exekveringstrådar.

Den operationella semantiken formaliseras i en bevisassistent for $µ$-kalkyl, VeriCode Proof Tool (VCPT). VCPT har utvecklats vid Swedish Institiute of Computer Science (SICS), och har kraftfulla tekniker för att bevisa induktiva påståenden.

Några exempel på bevis av egenskaper hos program användandes formaliseringen presenteras också.

Place, publisher, year, edition, pages
2005. , 111 p.
Series
IMIT/LECS, 2005-70
Keyword [en]
formal methods, semantics, verification, multi-threaded semantics
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-9512OAI: oai:DiVA.org:kth-9512DiVA: diva2:114295
Presentation
2005-04-28, Gemini, Forum, Isafjordsgatan 39, Kista, 10:15 (English)
Uppsok
Technology
Supervisors
Examiners
Available from: 2009-02-25 Created: 2008-11-11 Last updated: 2014-10-15

Open Access in DiVA

fulltext(791 kB)1110 downloads
File information
File name FULLTEXT01.pdfFile size 791 kBChecksum SHA-512
6d0fba3700ebd5ec46ee1d471253cdfe22a5fe5d9df01f96c20120bdef19e337ed190d4a252a209349901330d76be5cbe19e1b913fef0632e33a2c1bdf03ae01
Type fulltextMimetype application/pdf

Other links

http://web.it.kth.se/~zayenz/exjobb/thesis.pdf

Search in DiVA

By author/editor
Lagerkvist, Mikael Zayenz
By organisation
Electronic, Computer and Software Systems, ECS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1110 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: 206 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • 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