TY - JOUR
AB - The prominent and evolutionarily ancient role of the plant hormone auxin is the regulation of cell expansion. Cell expansion requires ordered arrangement of the cytoskeleton but molecular mechanisms underlying its regulation by signalling molecules including auxin are unknown. Here we show in the model plant Arabidopsis thaliana that in elongating cells exogenous application of auxin or redistribution of endogenous auxin induces very rapid microtubule re-orientation from transverse to longitudinal, coherent with the inhibition of cell expansion. This fast auxin effect requires auxin binding protein 1 (ABP1) and involves a contribution of downstream signalling components such as ROP6 GTPase, ROP-interactive protein RIC1 and the microtubule-severing protein katanin. These components are required for rapid auxin-and ABP1-mediated re-orientation of microtubules to regulate cell elongation in roots and dark-grown hypocotyls as well as asymmetric growth during gravitropic responses.
AU - Chen, Xu
AU - Grandont, Laurie
AU - Li, Hongjiang
AU - Hauschild, Robert
AU - Paque, Sébastien
AU - Abuzeineh, Anas
AU - Rakusová, Hana
AU - Benková, Eva
AU - Perrot Rechenmann, Catherine
AU - Friml, Jirí
ID - 1862
IS - 729
JF - Nature
TI - Inhibition of cell expansion by rapid ABP1-mediated auxin effect on microtubules
VL - 516
ER -
TY - CONF
AB - 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.
AU - Hofferek, Georg
AU - Gupta, Ashutosh
ED - Yahav, Eran
ID - 1869
T2 - HVC 2014
TI - Suraq - a controller synthesis tool using uninterpreted functions
VL - 8855
ER -
TY - CONF
AB - We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers.
AU - Henzinger, Thomas A
AU - Otop, Jan
AU - Samanta, Roopsha
ID - 1870
T2 - Leibniz International Proceedings in Informatics, LIPIcs
TI - Lipschitz robustness of finite-state transducers
VL - 29
ER -
TY - CONF
AB - 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.
AU - Gupta, Ashutosh
AU - Kovács, Laura
AU - Kragl, Bernhard
AU - Voronkov, Andrei
ED - Cassez, Franck
ED - Raskin, Jean-François
ID - 1872
T2 - ATVA 2014
TI - Extensional crisis and proving identity
VL - 8837
ER -
TY - CONF
AB - We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.
AU - Samanta, Roopsha
AU - Olivo, Oswaldo
AU - Allen, Emerson
ED - Müller-Olm, Markus
ED - Seidl, Helmut
ID - 1875
TI - Cost-aware automatic program repair
VL - 8723
ER -