Concept

Deductive reasoning

Related publications (109)

A Decision Procedure for (Co)datatypes in SMT Solvers

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure deci ...

Springer-Verlag Berlin2015

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

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

Viktor Kuncak, Régis William Blanc

We extend the Leon verification system for Scala with support for bit-vector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved i ...

ACM Press2015

Formal verification of infinite-state BIP models

Simon Bliudze, Wajeb Saab

We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose con- siderable restrictions: they ...

Springer2015

Scalable and Reactive Programming for Semantic Web Developers

Jean Paul Calbimonte Perez

The Semantic Web brings a powerful set of concepts, standards and ideas that are already changing the shape of the Web. However, in order to put these notions into practice we need to translate them into code. That is why the broad notion of programming th ...

CEUR-WS2015

Performance Assessment and Prognosis for Civil Infrastructure Based on Model Falsification Reasoning

Romain Pasquier

Infrastructure facilities are important to the economic growth and quality of life of modern societies. Much infrastructure has been built principally in the second half of the 20th century and several thousand structures are now attaining their design liv ...

EPFL2015

Statistics of Extremes

Anthony Christopher Davison, Raphaël Huser

Statistics of extremes concerns inference for rare events. Often the events have never yet been observed, and their probabilities must therefore be estimated by extrapolation of tail models fitted to available data. Because data concerning the event of int ...

Annual Reviews2015

Kullback-Leibler Proximal Variational Inference

Pascal Fua, François Fleuret, Pierre Bruno Baqué, Mohammad Emtiyaz Khan

We propose a new variational inference method based on a proximal framework that uses the Kullback-Leibler (KL) divergence as the proximal term. We make two contributions towards exploiting the geometry and structure of the variational bound. Firstly, we p ...

2015

Response to "Critical Assessment of the Evidence for Striped Nanoparticles"

Francesco Stellacci, Quy Ong Khac

Stirling et al., (10.1371/journal.pone.0108482) presented an analysis on some of our publications on the formation of stripe-like domains on mixed-ligand coated gold nanoparticles. The authors shed doubts on some of our results however no valid argument is ...

Public Library of Science2015

Towards Ontology-Based Modeling of Technical Documentation and Operation Data of the Engineering Asset

Drazen Nadoveza, Andreas Koukias

Management of engineering assets within an organization is a crucial interdisciplinary approach that aims to optimize their performance and guarantee their overall effectiveness through efficient decision making. This task is always largely supported by of ...

Springer-Verlag Berlin2015

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.