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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:30: Case StudiesVMCAI at VMCAI
Chair(s): Roderick BloemInstitute of Software Technology, Graz University of Technology
18:00 - 18:15
Formal Semantics and Verification of Network Based Biocomputation Circuits
Michelle Aluf-MedinaBar Ilan University, Till KortenTU Dresden, Avraham RavivBar Ilan University, Dan Nicolau Jr.Molecular Sense, Hillel KuglerBar Ilan University
Media Attached
18:15 - 18:30
Netter: Probabilistic, Stateful Network Models
Han ZhangCarnegie Mellon University, Chi Zhang, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Yuvraj AgarwalCarnegie Mellon University, Matt FredriksonCarnegie Mellon University, Limin JiaCarnegie Mellon University
Media Attached