uu.seUppsala University Publications

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt149",{id:"formSmash:upper:j_idt149",widgetVar:"widget_formSmash_upper_j_idt149",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt150_j_idt152",{id:"formSmash:upper:j_idt150:j_idt152",widgetVar:"widget_formSmash_upper_j_idt150_j_idt152",target:"formSmash:upper:j_idt150:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Approximations and abstractions for reasoning about machine arithmeticPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
2016 (English)Licentiate thesis, comprehensive summary (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Uppsala University, 2016.
##### Series

Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2016-010
##### National Category

Computer Sciences
##### Research subject

Computer Science with specialization in Embedded Systems
##### Identifiers

URN: urn:nbn:se:uu:diva-305190OAI: oai:DiVA.org:uu-305190DiVA, id: diva2:1034570
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt443",{id:"formSmash:j_idt443",widgetVar:"widget_formSmash_j_idt443",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt449",{id:"formSmash:j_idt449",widgetVar:"widget_formSmash_j_idt449",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt455",{id:"formSmash:j_idt455",widgetVar:"widget_formSmash_j_idt455",multiple:true});
##### Projects

UPMARCAvailable from: 2016-10-12 Created: 2016-10-12 Last updated: 2019-02-25Bibliographically approved
##### List of papers

Safety-critical systems rely on various forms of machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic. The problem with machine arithmetic is that it can exhibit subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. Failure of safety-critical systems is unacceptable, because it can cost lives or huge amounts of money, time and effort. To prevent such incidents, we want to formally prove that systems satisfy certain safety properties, or otherwise discover cases when the properties are violated. However, for this we need to be able to formally reason about machine arithmetic. The main problem with existing approaches is their inability to scale well with the increasing complexity of systems and their properties. In this thesis, we explore two alternatives to bit-blasting, the core procedure lying behind many common approaches to reasoning about machine arithmetic.

In the first approach, we present a general approximation framework which we apply to solve constraints over floating-point arithmetic. It is built on top of an existing decision procedure, e.g., bit-blasting. Rather than solving the original formula, we solve a sequence of approximations of the formula. Initially very crude, these approximations are frequently solved very quickly. We use results from these approximations to either obtain a solution, obtain a proof of unsatisfiability or generate a new approximation to solve. Eventually, we will either have found a solution or a proof that solution does not exist. The approximation framework improves the solving time and can solve a number of formulas that the bit-blasting cannot.

In the second approach, we present a novel method to reason about the theory of fixed-width bit-vectors. This new decision procedure is called mcBV and it is based on the model constructing satisfiability calculus (mcSAT). The procedure uses a lazy representation of bit-vectors and attempts to avoid bit-blasting altogether. It is able to reason about bit-vectors on both bit- and word-level, leveraging both Boolean constraint propagation and native arithmetic reasoning. It also features a greedy explanation generalization mechanism and is capable of more general learning compared to existing approaches. mcBV is able to reason about bit-vectors with sizes that significantly exceed the usual 32, 64 and 128 bits. Evaluation of mcBV shows an improvement in performance (compared to bit-blasting) on several classes of problems.

1. An approximation framework for solvers and decision procedures$(function(){PrimeFaces.cw("OverlayPanel","overlay1034538",{id:"formSmash:j_idt505:0:j_idt509",widgetVar:"overlay1034538",target:"formSmash:j_idt505:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. Deciding bit-vector formulas with mcSAT$(function(){PrimeFaces.cw("OverlayPanel","overlay1034553",{id:"formSmash:j_idt505:1:j_idt509",widgetVar:"overlay1034553",target:"formSmash:j_idt505:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

urn-nbn$(function(){PrimeFaces.cw("Tooltip","widget_formSmash_j_idt1171",{id:"formSmash:j_idt1171",widgetVar:"widget_formSmash_j_idt1171",showEffect:"fade",hideEffect:"fade",showDelay:500,hideDelay:300,target:"formSmash:altmetricDiv"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1225",{id:"formSmash:lower:j_idt1225",widgetVar:"widget_formSmash_lower_j_idt1225",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1226_j_idt1228",{id:"formSmash:lower:j_idt1226:j_idt1228",widgetVar:"widget_formSmash_lower_j_idt1226_j_idt1228",target:"formSmash:lower:j_idt1226:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});