The modelling and synthesis of chemical reaction networks by Whitby, M

Subjects:

Automated concurrency bug finding using partial-orders by Horn, A

“…This separation opens up a fresh and fruitful algorithmic perspective on partial-order encodings, including a new partial-order encoding that can drastically reduce the run-time of the analysis prior to calling the SAT/SMT solver, and new insights into the exponential worst-case time complexity of partial-order encodings during SAT/SMT solving. …”

Syntax-guided optimal synthesis for chemical reaction networks by Cardelli, L, Ceska, M, Fraenzle, M, Kwiatkowska, M, Laurenti, L, Paoletti, N, Whitby, M

“…We design and implement a novel algorithm for the optimal synthesis of CRNs that employs almost complete refutation procedure for SMT over reals and ODEs, and exploits a meta-sketching abstraction controlling the search strategy. …”

Safety verification of deep neural networks by Huang, X, Kwiatkowska, M, Wang, S, Wu, M

“…We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on safety of image classification decisions with respect to image manipulations, such as scratches or changes to camera angle or lighting conditions that would result in the same class being assigned by a human, and define safety for an individual decision in terms of invariance of the classification within a small neighbourhood of the original image. …”

Automatic verification of concurrent stochastic systems by Kwiatkowska, M, Parker, D, Norman, G, Santos, G

“…For zerosum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool’s modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.…”

Automatic verification and strategy synthesis for zero-sum and equilibria properties of concurrent stochastic games by Santos, GHR

“…Our model checking algorithms for a variant of stopping games make use of linear and nonlinear optimisation along with SMT solvers and are able to verify zero-sum and nonzero-sum properties of concurrent stochastic models. …”