IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series (S3)

Software Seminar Series (S3)

Zachary Grannan

Tuesday, July 21, 2020

11:00am https://zoom.us/j/7911012202 (pass: S3)

Zachary Grannan, Research Intern, IMDEA Software Institute

REST: Rewriting for SMT Verification with User-Defined Functions

Abstract:

We introduce REST, a rewrite technique for SMT-based verifiers that supports user-defined terminating functions. Our technique builds upon proof-by-logical evaluation (PLE) that decidably encodes user-defined functions as SMT equalities. REST extends PLE to automatically instantiate provably correct rewrite rules. It uses size-change termination to ensure that rewriting does not diverge, preserving predictable verification. We implement REST in Liquid Haskell and use it to automate proof generation. The automation provided by REST sets the ground for further proof tactic development: we used metaprogramming to implement a structural induction tactic. Our evaluation of REST and the induction tactic combined concludes that 1) they are not subsumed by existing rewriting techniques, 2) they can automate existing proof benchmarks, and 3) having the expected verification slowdown cost, they greatly ease Liquid Haskell proof development.


Time and place:
11:00am https://zoom.us/j/7911012202 (pass: S3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Zsolt Istvan

Tuesday, June 23, 2020

11:00am https://zoom.us/j/7911012202 (pass: S3)

Zsolt Istvan, Assistant Research Professor, IMDEA Software Institute

The Good, The Bad and the Road Ahead: Hardware Acceleration for BFT Consensus

Abstract:

Permissioned blockchains can offer a mechanism for transacting across several, not necessarily trusting, entities but they are often not reaching high performance due to the cost of the underlying consensus protocols. When deploying these systems in fast networking environments, there is an opportunity for acceleration by considering all available hardware features, such as FPGAs, programmable NICs and switches, to reduce consensus cost. In this talk, I will provide an overview of Permissioned Blockchains, their use of Byzantine fault tolerant (BFT) consensus protocols, and then deconstruct one such protocol with the goal of forecasting the benefits of various acceleration strategies.


Time and place:
11:00am https://zoom.us/j/7911012202 (pass: S3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Elena Gutierrez

Tuesday, June 16, 2020

11:00am https://zoom.us/j/7911012202 (pass: S3)

Elena Gutierrez, PhD Student, IMDEA Software Institute

A Congruence-based Perspective on Automata Minimization Algorithms

Abstract:

Getting the deterministic finite-state automaton with the least possible number of states is an essential question in many applications such as text processing, image analysis, program verification and synthesis. Most of the minimization methods that have been proposed in the literature rely on building a partition of the set of states of the input automaton to obtain the minimal deterministic automaton. This is the case of Hopcroft's and Moore's algorithm. Another independent method is the classical textbook procedure proposed by Brzozowski. This algorithm simply combines a determinization (D) and reverse (R) operation twice applied to the input automaton N, i.e., D○R○D○R(N), to obtain the minimal automaton. Despite having an exponential worst-case complexity, its simplicity has recently motivated the study of this method and its connection with the partition-based methods, with the goal of providing more efficient versions of it. In this talk, I will address this study from a language-theoretical perspective. I will use equivalence relations on words to give a new and simple proof of correctness of the double-reversal method and shed light on the connection between this method and Moore's algorithm, a partition-based method. This is the result of a joint work with Pedro Valero and Pierre Ganty, that I presented at MFCS last year.


Time and place:
11:00am https://zoom.us/j/7911012202 (pass: S3)
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Winter 2020