Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 18:00 - 18:15 at VMCAI - Case Studies Chair(s): Roderick Bloem

Network-Based Biocomputation Circuits (NBCs) offer a new paradigm for solving complex computational problems by utilizing biological agents that operate in parallel to explore manufactured planar devices. The approach can also have future applications in diagnostics and medicine by combining NBCs computational power with the ability to interface with biological material. To realize this potential, devices should be designed in a way that ensures their correctness and robust operation. For this purpose, formal methods and tools can offer significant advantages by allowing investigation of design limitations and detection of errors before manufacturing and experimentation. Here we define a computational model for NBCs by providing formal semantics to NBC circuits. We present a formal verification-based approach and prototype tool that can assist in the design of NBCs by enabling verification of a given design’s correctness. Our tool allows verification of the correctness of NBC designs for several NP-Complete problems, including the Subset Sum, Exact Cover and Satisfiability problems and can be extended to other NBC implementations. Our approach is based on defining transition systems for NBCs and using temporal logic for specifying and proving properties of the design using model checking. Our formal model can also serve as a starting point for computational complexity studies of the power and limitations of NBC systems.

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:30
Case StudiesVMCAI at VMCAI
Chair(s): Roderick Bloem Institute of Software Technology, Graz University of Technology
18:00
15m
Talk
Formal Semantics and Verification of Network Based Biocomputation Circuits
VMCAI
Michelle Aluf-Medina Bar Ilan University, Till Korten TU Dresden, Avraham Raviv Bar Ilan University, Dan Nicolau Jr. Molecular Sense, Hillel Kugler Bar Ilan University
Media Attached
18:15
15m
Talk
Netter: Probabilistic, Stateful Network Models
VMCAI
Han Zhang Carnegie Mellon University, Chi Zhang , Arthur Azevedo de Amorim Carnegie Mellon University, USA, Yuvraj Agarwal Carnegie Mellon University, Matt Fredrikson Carnegie Mellon University, Limin Jia Carnegie Mellon University
Media Attached