Automated theorem proving

Related publications (30)

About
Privacy
Disclaimer

Graph Chatbot

Verification of Software Network Functions with No Verification Expertise

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

The First Passage Sets of the 2D Gaussian Free Field: Convergence and Isomorphisms

Juhan Aru, Titus Lupu

In a previous article, we introduced the first passage set (FPS) of constant level -aof the two-dimensional continuum Gaussian free field (GFF) on finitely connected domains. Informally, it is the set of points in the domain that can be connected to the bo ...

SPRINGER2020

Nonintrusive and Adaptive Monitoring for Locating Voltage Attacks in Virtualized FPGAs

Mirjana Stojilovic, Andrea Guerrieri, Seyedeh Sharareh Mirzargar, Gaiëtan Renault

In this work, we present an automated approach for locating power-wasting attackers in shared FPGAs. In this approach, the FPGA shell is responsible for, first, placing the user designs and, second, inserting voltage sensors in a nonintrusive and adaptive ...

IEEE COMPUTER SOC2020

A scalable, line-independent control design algorithm for voltage and frequency stabilization in AC islanded microgrids

Giancarlo Ferrari Trecate, Michele Tucci

We propose a decentralized control synthesis procedure for stabilizing voltage and frequency in AC Islanded microGrids (ImGs) composed of Distributed Generation Units (DGUs) and loads interconnected through power lines. The presented approach enables Plug- ...

2020

Seek and learn: Automated identification of microevents in animal behaviour using envelopes of acceleration data and machine learning

Kamiar Aminian, Hooman Dejnabadi, Pritish Chakravarty

Animal‐borne accelerometers have been used across more than 120 species to infer biologically significant information such as energy expenditure and broad behavioural categories. While the accelerometer’s high sensitivity to movement and fast response time ...

2020

Refutation-based synthesis in SMT

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

SPRINGER2019

Sign-Changing Solutions for a Class of Zero Mass Nonlocal Schrodinger Equations

We consider the following class of fractional Schrodinger equations: (-Delta)(alpha)u + V(x)u = K(x)f(u) in R-N, where alpha is an element of (0, 1), N > 2 alpha, (-Delta)(alpha) is the fractional Laplacian, V and K are positive continuous functions which ...

2019

Stability Analysis of Primary Plug-and-Play and Secondary Leader-Based Controllers for DC Microgrid Clusters

Giancarlo Ferrari Trecate, Michele Tucci, Andrea Martinelli, Renke Han

In this paper, we propose a new hierarchical control scheme for microgrid (MG) clusters, given by the interconnection of atomic dc MGs with ZIP loads, each composed by both grid-forming and grid-feeding converters. In the primary level, we develop a new Pl ...

IEEE Institute of Electrical and Electronics Engineers2019

FCR: Fast and Consistent Controller-Replication in Software Defined Networking

Jean-Yves Le Boudec, Eleni Stai, Mia Primorac, Maaz Mashood Mohiuddin

We consider the problem of coordination among replicated SDN controllers, where the challenge is to ensure a consistent view of the network while reacting to network events in a prompt manner. Existing solutions are either consensus-based, which achieve co ...

2019

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

Page 3 of 3

Seek and learn: Automated identification of microevents in animal behaviour using envelopes of acceleration data and machine learning

Kamiar Aminian, Hooman Dejnabadi, Pritish Chakravarty

2020