Publications related to Formal verification

Formal Verification of Rust with Stainless

Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...

2021

Direct Model-checking of SysML Models

Alessandro Tempia Calvino

Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a ne ...

SCITEPRESS2021

Convergence of adaptive algorithms for constrained weakly convex optimization

Volkan Cevher, Ahmet Alacaoglu, Yurii Malitskyi

We analyze the adaptive first order algorithm AMSGrad, for solving a constrained stochastic optimization problem with a weakly convex objective. We prove the

\tilde O(t^{-1/2})

rate of convergence for the squared norm of the gradient of Moreau envelope, ...

2021

Proof of Multi-Stage Programming with Generative and Analytical Macros

Martin Odersky, Nicolas Alexander Stucki, Jonathan Immanuel Brachthäuser

In metaprogramming, code generation and code analysis are complementary. Traditionally, principled metaprogramming extensions for programming languages, like MetaML and BER MetaOCaml, offer strong foundations for code generation but lack equivalent support ...

EPFL2021

A Simpler and Faster NIC Driver Model for Network Functions

George Candea, Solal Vincenzo Pirelli

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that p ...

2021

Edit Based Grading of SQL Queries

Bikash Chandra

Grading student SQL queries manually is a tedious and error-prone process. Earlier work on testing correctness of student SQL queries, such as the XData system, can be used to test the correctness of a student query. However, in case a student query is fou ...

ASSOC COMPUTING MACHINERY2021

Method and system for determining the intention of performing a voluntary action

Olaf Blanke, Bastien Orset

The invention relates to methods and systems for determining the intention of a subject to perform a voluntary action based on the analysis of the subject's respiratory phases and neuroelectrical signals. ...

2021

A Modular Workflow for Model Building, Analysis, and Parameter Estimation in Systems Biology and Neuroscience

Daniel Keller, Andrii Stepaniuk

Neuroscience incorporates knowledge from a range of scales, from single molecules to brain wide neural networks. Modeling is a valuable tool in understanding processes at a single scale or the interactions between two adjacent scales and researchers use a ...

HUMANA PRESS INC2021

Learning convergence prediction of astrobots in multi-object spectrographs

Denis Gillet, Jean-Paul Richard Kneib, Matin Macktoobian, Francesco Basciani

Astrobot swarms are used to capture astronomical signals to generate the map of the observable universe for the purpose of dark energy studies. The convergence of each swarm in the course of its coordination has to surpass a particular threshold to yield a ...

2021

Cortical Surfaces Integration with Tractography for Structural Connectivity Analysis

Gabriel Girard, Maxime Descoteaux

Background: Mapping diffusion MRI tractography streamlines to the cortical surface facilitates the integration of white matter features onto gray matter, especially for connectivity analysis. Method: In this work, we present methods that combine cortical s ...

MARY ANN LIEBERT, INC2021

Formal verification

Graph Chatbot

Chat with Graph Search

Formal Verification of Rust with Stainless

Direct Model-checking of SysML Models

Convergence of adaptive algorithms for constrained weakly convex optimization

Proof of Multi-Stage Programming with Generative and Analytical Macros

A Simpler and Faster NIC Driver Model for Network Functions

Edit Based Grading of SQL Queries

Method and system for determining the intention of performing a voluntary action

A Modular Workflow for Model Building, Analysis, and Parameter Estimation in Systems Biology and Neuroscience

Learning convergence prediction of astrobots in multi-object spectrographs

Cortical Surfaces Integration with Tractography for Structural Connectivity Analysis

Formal Verification of Rust with Stainless

Direct Model-checking of SysML Models

Proof of Multi-Stage Programming with Generative and Analytical Macros

A Simpler and Faster NIC Driver Model for Network Functions

Edit Based Grading of SQL Queries

Convergence of adaptive algorithms for constrained weakly convex optimization

Method and system for determining the intention of performing a voluntary action

A Modular Workflow for Model Building, Analysis, and Parameter Estimation in Systems Biology and Neuroscience

Learning convergence prediction of astrobots in multi-object spectrographs

Cortical Surfaces Integration with Tractography for Structural Connectivity Analysis