@article{494, abstract = {We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata.}, author = {Boker, Udi and Kupferman, Orna}, journal = {ACM Transactions on Computational Logic (TOCL)}, number = {4}, publisher = {ACM}, title = {{Translating to Co-Büchi made tight, unified, and useful}}, doi = {10.1145/2362355.2362357}, volume = {13}, year = {2012}, } @article{3249, abstract = {Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability". We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.}, author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun}, journal = {Theoretical Computer Science}, number = {1}, pages = {21 -- 35}, publisher = {Elsevier}, title = {{Simulation distances}}, doi = {10.1016/j.tcs.2011.08.002}, volume = {413}, year = {2012}, } @inproceedings{10903, abstract = {We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.}, author = {Bouajjani, Ahmed and Dragoi, Cezara and Enea, Constantin and Sighireanu, Mihaela}, booktitle = {Automated Technology for Verification and Analysis}, isbn = {9783642333859}, issn = {1611-3349}, location = {Thiruvananthapuram, India}, pages = {167--182}, publisher = {Springer}, title = {{Accurate invariant checking for programs manipulating lists and arrays with infinite data}}, doi = {10.1007/978-3-642-33386-6_14}, volume = {7561}, year = {2012}, } @inproceedings{10906, abstract = {HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.}, author = {Grebenshchikov, Sergey and Gupta, Ashutosh and Lopes, Nuno P. and Popeea, Corneliu and Rybalchenko, Andrey}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, editor = {Flanagan, Cormac and König, Barbara}, isbn = {9783642287558}, issn = {1611-3349}, location = {Tallinn, Estonia}, pages = {549--551}, publisher = {Springer}, title = {{HSF(C): A software verifier based on Horn clauses}}, doi = {10.1007/978-3-642-28756-5_46}, volume = {7214}, year = {2012}, } @inbook{5745, author = {Gupta, Ashutosh}, booktitle = {Automated Technology for Verification and Analysis}, isbn = {9783642333859}, issn = {1611-3349}, location = {Thiruvananthapuram, Kerala, India}, pages = {107--121}, publisher = {Springer Berlin Heidelberg}, title = {{Improved Single Pass Algorithms for Resolution Proof Reduction}}, doi = {10.1007/978-3-642-33386-6_10}, volume = {7561}, year = {2012}, }