Publication

Sound reasoning about integral data types with a reusable SMT solver interface

Related publications (33)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Many-body perturbation theory calculations using the yambo code

Antimo Marrazzo, Gianluca Prandini, Andrea Ferretti

yambo is an open source project aimed at studying excited state properties of condensed matter systems from first principles using many-body methods. As input, yambo requires ground state electronic structure data as computed by density functional theory c ...

IOP PUBLISHING LTD2019

Induction for SMT Solvers

Viktor Kuncak, Andrew Joseph Reynolds

Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas ...

Springer-Verlag Berlin2015

Obey: Code Health for Scala.Meta

Adrien Ghosn, Eugene Burmako

Obey is a user-friendly tool that helps programmers enforce code health requirements in their projects. Requirements are expressed as rules, written with the TQL library combinators used to traverse scala.meta trees, that generate compiler warnings and can ...

2015

Improving Scalability of Symbolic Execution for Software with Complex Environment Interfaces

Stefan Bucur

Manual software testing is laborious and prone to human error. Yet, among practitioners, it is the most popular method for quality assurance. Automating the test case generation promises better effectiveness, especially for exposing corner-case bugs. Symbo ...

EPFL2015

CM values of higher Green's functions and regularized Petersson products

Maryna Viazovska

Higher Green functions are real-valued functions of two variables on the upper half-plane, which are bi-invariant under the action of a congruence subgroup, have a logarithmic singularity along the diagonal, and satisfy the equation f = k(1−k) f ; here i ...

Cambridge UP2015

Photogrammetric Mission Planner for RPAS

Jan Skaloud, Martin Rehak, Florian Gandor

This paper presents a development of an open-source flight planning tool for Remotely Piloted Aircraft Systems (RPAS) that is dedicated to high-precision photogrammetric mapping. This tool contains planning functions that are usually available in professio ...

2015

On Induction for SMT Solvers

Viktor Kuncak, Andrew Joseph Reynolds

2014

Computing in social networks

Rachid Guerraoui, Anne-Marie Kermarrec, Kévin Clément Huguenin, Andrei Giurgiu

This paper defines the problem of Scalable Secure computing in a Social network: we call it the S-3 problem. In short, nodes, directly reflecting on associated users, need to compute a symmetric function f : V-n -> U of their inputs in a set of constant si ...

Elsevier2014

Interpolation for Synthesis on Unbounded Domains

Viktor Kuncak, Régis William Blanc

Synthesis procedures compile relational specifications into functions. In addition to bounded domains, synthesis procedures are applicable to domains such as mathematical integers, where the domain and range of relations and synthesized code is unbounded. ...

Ieee2013

Miniboxing: An Encoding for Specialization

Cristian Talau

In the presence of parametric polymorphism, erasure-based languages such as Java and Scala handle primitives (boolean values, integers and floating point numbers) in a suboptimal way: in order to provide a uniform representation on the low level, all primi ...

2012