MUNCH - Automated Reasoner for Sets and Multisets

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.

Agent-based simulations have been widely applied in many disciplines, by scientists and engineers alike. Scientists use agent-based simulations to tackle global problems, including alleviating poverty, reducing violence, and predicting the impact of pandem ...

This paper studies the problem of online performance optimization of constrained closed-loop control systems, where both the objective and the constraints are unknown black-box functions affected by exogenous time-varying contextual disturbances. A primal- ...

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 ...

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

Machine intelligence greatly impacts almost all domains of our societies. It is profoundly changing the field of mechanical engineering with new technical possibilities and processes. The education of future engineers also needs to adapt in terms of techni ...

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various impl ...

Many different data analytics tasks boil down to linear algebra primitives. In practice, for each different type of workload, data scientists use a particular specialised library. In this paper, we present Pilatus, a polymorphic iterative linear algebra la ...

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy various constraints. In this thesis, we demonstrate how for ...

The most successful systems for "big data'' processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate, or middleware, upon which to build data-centric distribute ...

Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model. Furthermore, they need to interact with other languages targeting said runtimes. A language targeting only one runtim ...

In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...

Boolean SAT solving can be used to find a minimum- size logic network for a given small Boolean function. This paper extends the SAT formulation to find a minimum-size network under delay constraints. Delay constraints are given in terms of input arrival t ...

Production compilers for programming languages face multiple requirements. They should be correct, as we rely on them to produce code. They should be fast, in order to provide a good developer experience. They should also be easy to maintain and evolve. Th ...

The major research in the resource management literature focuses primarily on two complementary sub-problems: (1) specification languages for formulating resource requests and (2) constraint problems modelling allocation and scheduling. Both directions ass ...

Due to recent advances, constraint solvers have become efficient tools for synthesizing optimum Boolean circuits. We take advantage of this by showing how SAT based exact synthesis may be used as a method for finding minimum length Boolean chains. As oppos ...

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs ...

The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on which to build data-centric distributed systems. A key id ...

MUNCH - Automated Reasoner for Sets and Multisets

Chat with Graph Search

Generalizing Bulk-Synchronous Parallel Processing for Data Science: From Data to Threads and Agent-Based Simulations

Primal-Dual Contextual Bayesian Optimization for Control System Online Optimization with Time-Average Constraints

Scaling Language Features for Program Verification

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Automated Verification of Network Function Binaries

Automated Design: A Journey Across Modelling, Optimization, and Education

Proving and Disproving Equivalence of Functional Programming Assignments

Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages

Finally, a Polymorphic Linear Algebra Language

Verified Functional Programming

Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization

A Programming Model and Foundation for Lineage-Based Distributed Computation

Cross-Platform Language Design

Verification by Reduction to Functional Programs

Busy Man’s Synthesis: Combinational Delay Optimization With SAT

Design and implementation of an optimizing type-centric compiler for a high-level language

Constraint-Flow Nets: A Model for Building Constraints from Resource Dependencies

Classifying Functions with Exact Synthesis

Translating Scala Programs to Isabelle/HOL, Automated Reasoning

Function Passing: A Model for Typed, Distributed Functional Programming