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
Presburger Arithmetic and Its Use in Verification.
KTH, School of Computer Science and Communication (CSC).
2011 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Phan Anh Dung

Presburger Arithmetic and its use in verification

Today, when every computer has gone multicore, the requirement of taking advantage of these computing powers becomes critical. However, multicore parallelism is complex and error-prone due to extensive use of synchronization techniques. In this thesis, we explore the functional paradigm in the context of F# programming language and parallelism support in .NET framework. This paradigm prefers the declarative way of thinking and no side effect which lead to the ease of parallelizing algorithms. The purpose is to investigate decision algorithms for quantified linear arithmetic of integers (also called Presburger Arithmetic) aiming at efficient parallel implementations. The context of the project is; however, to support model checking for the real-time logic Duration Calculus, and the goal is to decide a subset of Presburger formulas, which is relevant to this model-checking problem and for which efficient tool support can be provided. We present a simplification process for this subset of Presburger formulas which gives some hope for creating smaller corresponding formulas. Later two parallel decision procedures for Presburger Arithmetic along with their experimental results are discussed.

Abstract [sv]

Phan Anh Dung

Presburgeraritmetik och dess användning i verifiering

Idag, när alla datorer har utrustats med flerkärniga processorer, har det blivit viktigt att ta tillvara den utökade beräkningskapaciteten som detta ger. Att utnyttja parallellism via flera processorkärnor är dock komplext och riskerar att leda till fel då synkroniseringstekniker används. I den här rapporten utforskar vi den funktionella paradigmen i kontexten av programmeringsspråket F# och dess stöd för parallellism i .NET Framework. Denna paradigm förordar ett deklarativt uttryckssätt och att sidoeffekter undviks, vilket leder till att algoritmer enkelt kan paralleliseras. Syftet är att undersöka beslutsalgoritmer för kvantifierad linjär aritmetik för heltal (också kallad Presburgeraritmetik), med sikte på effektiva parallella implementationer. Arbetet ingår i utvecklingen av en modellprovare för realtidslogiken Duration Calculus och har som mål att kunna avgöra den delmängd av Presburgerformlerna som är relevant för detta modellprovningsproblem, och som effektiva verktyg kan ges för. Vi presenterar en förenklingsprocess för denna delmängd Presburgerformler, som ger visst hopp om att skapa ekvivalenta formler av liten storlek. Därefter diskuteras två parallella beslutsprocedurer för Presburgeraritmetik och tillhörande experimentella resultat.

Place, publisher, year, edition, pages
2011.
Series
Trita-CSC-E, ISSN 1653-5715 ; 2011:108
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-130752OAI: oai:DiVA.org:kth-130752DiVA: diva2:654199
Educational program
Master of Science -Security and Mobile Computing
Uppsok
Technology
Supervisors
Examiners
Available from: 2013-10-07 Created: 2013-10-07

Open Access in DiVA

No full text

Other links

http://www.nada.kth.se/utbildning/grukth/exjobb/rapportlistor/2011/rapporter11/phan_dung_11108.pdf
By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 23 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