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});});

From Machine Arithmetic to Approximations and back again: Improved SMT Methods for Numeric Data TypesPrimeFaces.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();
}
}
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

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

Uppsala: Acta Universitatis Upsaliensis, 2017. , p. 55
##### Series

Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1603
##### Keywords [en]

SMT, Model construction, Approximations, floating-point arithmetic, machine arithmetic, bit-vectors
##### National Category

Computer Sciences
##### Research subject

Computer Science
##### Identifiers

URN: urn:nbn:se:uu:diva-334565ISBN: 978-91-513-0162-4 (print)OAI: oai:DiVA.org:uu-334565DiVA, id: diva2:1159882
##### Public defence

2018-01-23, ITC/2446, Lägerhyddsvägen 2, Uppsala, 09:00 (English)
##### Opponent

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}); Available from: 2017-12-19 Created: 2017-11-24 Last updated: 2018-03-08
##### List of papers

Safety-critical systems, especially those found in avionics and automotive industries, rely on machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic exhibits subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. Failure of safety-critical systems is unacceptable, due to high-stakes involving human lives or huge amounts of money, time and effort. By formally proving properties of systems, we can be assured that they meet safety requirements. However, to prove such properties it is necessary to reason about machine arithmetic. SMT techniques for machine arithmetic are lacking scalability. This thesis presents approaches that augment or complement existing SMT techniques for machine arithmetic.

In this thesis, we explore approximations as a means of augmenting existing decision procedures. A general approximation refinement framework is presented, along with its implementation called UppSAT. The framework solves a sequence of approximations. Initially very crude, these approximations are fairly easy to solve. Results of solving approximate constraints are used to either reconstruct a solution of original constraints, obtain a proof of unsatisfiability or to refine the approximation. The framework preserves soundness, completeness, and termination of the underlying decision procedure, guaranteeing that eventually, either a solution is found or a proof that solution does not exist. We evaluate the impact of approximations implemented in the UppSAT framework on the state-of-the-art in SMT for floating-point arithmetic.

A novel method to reason about the theory of fixed-width bit-vectors called mcBV is presented. It is an instantiation of the model constructing satisfiability calculus, mcSAT, and uses a new lazy representation of bit-vectors that allows both bit- and word-level reasoning. It uses a greedy explanation generalization mechanism capable of more general learning compared to traditional approaches. Evaluation of mcBV shows that it can outperform bit-blasting on several classes of problems.

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

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

3. Exploring Approximations for Floating-Point Arithmetic using UppSAT$(function(){PrimeFaces.cw("OverlayPanel","overlay1159879",{id:"formSmash:j_idt505:2:j_idt509",widgetVar:"overlay1159879",target:"formSmash:j_idt505:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

isbn
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});});