Publications related to Refinement Propagation. Towards Automated Construction of Visual Specifications

Related publications (31)

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Yichen Xu

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

Smart Proofs via Recursive Information Gathering: Decentralized Refereeing by Smart Contracts

Clément Hongler

We introduce the SPRIG (Smart Proofs via Recursive Information Gathering) protocol. SPRIG allows agents to propose, question, and defend mathematical proofs in a decentralized fashion. A structure of stakes and bounties aims at producing debates in good fa ...

Association for Computing Machinery (ACM)2024

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Infusing structured knowledge priors in neural models for sample-efficient symbolic reasoning

Mattia Atzeni

The ability to reason, plan and solve highly abstract problems is a hallmark of human intelligence. Recent advancements in artificial intelligence, propelled by deep neural networks, have revolutionized disciplines like computer vision and natural language ...

EPFL2024

Chat2Code: A Chatbot for Model Specification and Code Generation, The Case of Smart Contracts

Shailesh Mishra

The potential of automatic code generation through Model-Driven Engineering (MDE) frameworks has yet to be realized. Beyond their ability to help software professionals write more accurate, reusable code, MDE frameworks could make programming accessible fo ...

Ieee Computer Soc2023

Monotonicity Reasoning in the Age of Neural Foundation Models

Zeming Chen

The recent advance of large language models (LLMs) demonstrates that these large-scale foundation models achieve remarkable capabilities across a wide range of language tasks and domains. The success of the statistical learning approach challenges our unde ...

Springer2023

Analysing the potential for modal shiftbased on the logic of modal choice

Vincent Kaufmann, Ludy Juliana González Villamizar, Eloi Antoine Maël Bernier, Florian Lucien Jacques Masse

This article explores how the logic underlying modal practices tends to modulate the population’s responsiveness to improvements in global transport supply. Based on a quantitative survey conducted in 2018–2019 among the working population of the cantons o ...

2023

Language Model Decoding as Likelihood–Utility Alignment

Frano Rajic, Jiheng Wei, Boi Faltings, Robert West, Maxime Jean Julien Peyrard, Debjit Paul, Valentin Hartmann, Martin Josifoski

A critical component of a successful language generation pipeline is the decoding algorithm. However, the general principles that should guide the choice of a decoding algorithm re- main unclear. Previous works only compare decoding algorithms in narrow sc ...

Assoc Computational Linguistics-Acl2023

Contextual Stochastic Bilevel Optimization

Daniel Kuhn, Andreas Krause, Yifan Hu

We introduce contextual stochastic bilevel optimization (CSBO) -- a stochastic bilevel optimization framework with the lower-level problem minimizing an expectation conditioned on some contextual information and the upper-level decision variable. This fram ...

2023

Climatic Affinities or Type As A Structure Of Relations, Based On Typological Transfer In The Work Of Lacaton & Vassal And Other Similar Precedents

Tiago André Pratas Borges

It is a generally accepted idea that typology is an essential element in the disciplinary dimension of architecture. The concept of typology, in its most common definition, is sufficiently malleable to cover a wide range of uses, but it is also this vaguen ...

2023

Climatic Affinities or Type As A Structure Of Relations Based On Typological Transfer In The Work Of Lacaton & Vassal And Other Similar Precedents

Tiago André Pratas Borges

It is a generally accepted idea that typology is an essential element in the disciplinary dimension of architecture. The concept of typology, in its most common definition, is sufficiently malleable to cover a wide range of uses, but it is also this vaguen ...

2023

Keep Sensors in Check: Disentangling Country-Level Generalization Issues in Mobile Sensor-Based Models with Diversity Scores

Daniel Gatica-Perez, Lakmal Buddika Meegahapola

Machine learning models trained with passive sensor data from mobile devices can be used to perform various inferences pertaining to activity recognition, context awareness, and health and well-being. Prior work has improved inference performance through t ...

Assoc Computing Machinery2023

Learning Transformations To Reduce the Geometric Shift in Object Detection

Mathieu Salzmann, Martin Pierre Engilberge, Vidit Vidit

The performance of modern object detectors drops when the test distribution differs from the training one. Most of the methods that address this focus on object appearance changes caused by, e.g., different illumination conditions, or gaps between syntheti ...

Ieee Computer Soc2023

Data-driven Methods for Control: from Linear to Lifting

Yingzhao Lian

The progress towards intelligent systems and digitalization relies heavily on the use of automation technology. However, the growing diversity of control objects presents significant challenges for traditional control approaches, as they are highly depende ...

EPFL2023

Overcoming decision paralysis—A digital twin for decision making in energy system design

François Maréchal, Julia Granacher, Tuong-Van Nguyen

The design of efficient energy systems, through the development of new technologies and the improvement of current ones, requires the use of rigorous process synthesis methods for generating and analysing design alternatives. We introduce a digital twin of ...

2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Textual Explanations and Critiques in Recommendation Systems

Diego Matteo Antognini

Artificial intelligence and machine learning algorithms have become ubiquitous. Although they offer a wide range of benefits, their adoption in decision-critical fields is limited by their lack of interpretability, particularly with textual data. Moreover, ...

EPFL2022

Decentralized in-order execution of a sequential task-based code for shared-memory architectures

Charly Nicolas Lucien Castes

The hardware complexity of modern machines makes the design of adequate programming models crucial for jointly ensuring performance, portability, and productivity in high-performance computing (HPC). Sequential task-based programming models paired with adv ...

IEEE COMPUTER SOC2022

Data-driven and Safe Networked Control with Applications to Microgrids

Mustafa Sahin Turan

Today, automatic control is integrated into a wide spectrum of real-world systems such as electrical grids and transportation networks. Many of these systems comprise numerous interconnected agents, perform safety-critical operations, or generate large amo ...

EPFL2022