@article{1351,
abstract = {The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.},
author = {Giacobbe, Mirco and Guet, Calin C and Gupta, Ashutosh and Henzinger, Thomas A and Paixao, Tiago and Petrov, Tatjana},
issn = {00015903},
journal = {Acta Informatica},
number = {8},
pages = {765 -- 787},
publisher = {Springer},
title = {{Model checking the evolution of gene regulatory networks}},
doi = {10.1007/s00236-016-0278-x},
volume = {54},
year = {2017},
}
@inproceedings{1230,
abstract = {Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average.},
author = {Daca, Przemyslaw and Gupta, Ashutosh and Henzinger, Thomas A},
location = {St. Petersburg, FL, USA},
pages = {328 -- 347},
publisher = {Springer},
title = {{Abstraction-driven concolic testing}},
doi = {10.1007/978-3-662-49122-5_16},
volume = {9583},
year = {2016},
}
@article{1808,
author = {Gupta, Ashutosh and Henzinger, Thomas A},
journal = {ACM Transactions on Modeling and Computer Simulation},
number = {2},
publisher = {ACM},
title = {{Guest editors' introduction to special issue on computational methods in systems biology}},
doi = {10.1145/2745799},
volume = {25},
year = {2015},
}
@inproceedings{1835,
abstract = {The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.},
author = {Giacobbe, Mirco and Guet, Calin C and Gupta, Ashutosh and Henzinger, Thomas A and Paixao, Tiago and Petrov, Tatjana},
location = {London, United Kingdom},
pages = {469 -- 483},
publisher = {Springer},
title = {{Model checking gene regulatory networks}},
doi = {10.1007/978-3-662-46681-0_47},
volume = {9035},
year = {2015},
}
@inproceedings{1992,
abstract = {We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.
We claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.
In the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula.},
author = {Gupta, Ashutosh and Henzinger, Thomas A and Radhakrishna, Arjun and Samanta, Roopsha and Tarrach, Thorsten},
isbn = {978-1-4503-3300-9},
location = {Mumbai, India},
pages = {433 -- 444},
publisher = {ACM},
title = {{Succinct representation of concurrent trace sets}},
doi = {10.1145/2676726.2677008},
year = {2015},
}
@inproceedings{1702,
abstract = {In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.},
author = {Gupta, Ashutosh and Popeea, Corneliu and Rybalchenko, Andrey},
booktitle = {Electronic Proceedings in Theoretical Computer Science, EPTCS},
location = {Vienna, Austria},
pages = {31 -- 38},
publisher = {Open Publishing},
title = {{Generalised interpolation by solving recursion free-horn clauses}},
doi = {10.4204/EPTCS.169.5},
volume = {169},
year = {2014},
}
@inproceedings{1869,
abstract = {Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes.},
author = {Hofferek, Georg and Gupta, Ashutosh},
booktitle = {HVC 2014},
editor = {Yahav, Eran},
location = {Haifa, Israel},
pages = {68 -- 74},
publisher = {Springer},
title = {{Suraq - a controller synthesis tool using uninterpreted functions}},
doi = {10.1007/978-3-319-13338-6_6},
volume = {8855},
year = {2014},
}
@inproceedings{1872,
abstract = {Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover.},
author = {Gupta, Ashutosh and Kovács, Laura and Kragl, Bernhard and Voronkov, Andrei},
booktitle = {ATVA 2014},
editor = {Cassez, Franck and Raskin, Jean-François},
location = {Sydney, Australia},
pages = {185 -- 200},
publisher = {Springer},
title = {{Extensional crisis and proving identity}},
doi = {10.1007/978-3-319-11936-6_14},
volume = {8837},
year = {2014},
}
@inbook{5747,
author = {Dragoi, Cezara and Gupta, Ashutosh and Henzinger, Thomas A},
booktitle = {Computer Aided Verification},
isbn = {9783642397981},
issn = {0302-9743},
location = {Saint Petersburg, Russia},
pages = {174--190},
publisher = {Springer Berlin Heidelberg},
title = {{Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates}},
doi = {10.1007/978-3-642-39799-8_11},
volume = {8044},
year = {2013},
}
@inproceedings{1385,
abstract = {It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results.},
author = {Hofferek, Georg and Gupta, Ashutosh and Könighofer, Bettina and Jiang, Jie and Bloem, Roderick},
booktitle = {2013 Formal Methods in Computer-Aided Design},
location = {Portland, OR, United States},
pages = {77 -- 84},
publisher = {IEEE},
title = {{Synthesizing multiple boolean functions using interpolation on a single proof}},
doi = {10.1109/FMCAD.2013.6679394},
year = {2013},
}
@inproceedings{2237,
abstract = {We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of examples over the theory of linear integer arithmetic and integer-indexed arrays, with and without quantifiers. When compared to other methods, our experiments show that some examples could only be solved by our implementation.},
author = {Blanc, Régis and Gupta, Ashutosh and Kovács, Laura and Kragl, Bernhard},
location = {Stellenbosch, South Africa},
pages = {173 -- 181},
publisher = {Springer},
title = {{Tree interpolation in Vampire}},
doi = {10.1007/978-3-642-45221-5_13},
volume = {8312},
year = {2013},
}
@proceedings{2288,
abstract = {This book constitutes the proceedings of the 11th International Conference on Computational Methods in Systems Biology, CMSB 2013, held in Klosterneuburg, Austria, in September 2013. The 15 regular papers included in this volume were carefully reviewed and selected from 27 submissions. They deal with computational models for all levels, from molecular and cellular, to organs and entire organisms.},
editor = {Gupta, Ashutosh and Henzinger, Thomas A},
isbn = {978-3-642-40707-9},
location = {Klosterneuburg, Austria},
publisher = {Springer},
title = {{Computational Methods in Systems Biology}},
doi = {10.1007/978-3-642-40708-6},
volume = {8130},
year = {2013},
}
@inproceedings{3136,
abstract = {Continuous-time Markov chains (CTMC) with their rich theory and efficient simulation algorithms have been successfully used in modeling stochastic processes in diverse areas such as computer science, physics, and biology. However, systems that comprise non-instantaneous events cannot be accurately and efficiently modeled with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that allows for the specification of a lower bound on the time interval between an event's initiation and its completion, and we propose an algorithm for the computation of their behavior. Our algorithm effectively decomposes the computation into two stages: a pure CTMC governs event initiations while a deterministic process guarantees lower bounds on event completion times. Furthermore, from the nature of delayed CTMCs, we obtain a parallelized version of our algorithm. We use our formalism to model genetic regulatory circuits (biological systems where delayed events are common) and report on the results of our numerical algorithm as run on a cluster. We compare performance and accuracy of our results with results obtained by using pure CTMCs. © 2012 Springer-Verlag.},
author = {Guet, Calin C and Gupta, Ashutosh and Henzinger, Thomas A and Mateescu, Maria and Sezgin, Ali},
location = {Berkeley, CA, USA},
pages = {294 -- 309},
publisher = {Springer},
title = {{Delayed continuous time Markov chains for genetic regulatory circuits}},
doi = {10.1007/978-3-642-31424-7_24},
volume = {7358 },
year = {2012},
}
@inproceedings{3264,
abstract = {Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.},
author = {Gupta, Ashutosh and Popeea, Corneliu and Rybalchenko, Andrey},
editor = {Yang, Hongseok},
location = {Kenting, Taiwan},
pages = {188 -- 203},
publisher = {Springer},
title = {{Solving recursion-free Horn clauses over LI+UIF}},
doi = {10.1007/978-3-642-25318-8_16},
volume = {7078},
year = {2011},
}
@inproceedings{4521,
abstract = {The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, the current focus of liveness verification has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite programexecution. In this paper, we propose a method to search for such counterexamples. The search proceeds in two phases. We first dynamically enumerate lasso-shaped candidate paths for counterexamples, and then statically prove their feasibility. We illustrate the utility of our nontermination prover, called TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations.},
author = {Ashutosh Gupta and Thomas Henzinger and Majumdar, Ritankar S and Rybalchenko, Andrey and Xu, Ru-Gang},
pages = {147 -- 158},
publisher = {ACM},
title = {{Proving non-termination}},
doi = {10.1145/1328438.1328459},
year = {2008},
}