@article{1854,
abstract = {In this paper, we present a method for non-rigid, partial shape matching in vector graphics. Given a user-specified query region in a 2D shape, similar regions are found, even if they are non-linearly distorted. Furthermore, a non-linear mapping is established between the query regions and these matches, which allows the automatic transfer of editing operations such as texturing. This is achieved by a two-step approach. First, pointwise correspondences between the query region and the whole shape are established. The transformation parameters of these correspondences are registered in an appropriate transformation space. For transformations between similar regions, these parameters form surfaces in transformation space, which are extracted in the second step of our method. The extracted regions may be related to the query region by a non-rigid transform, enabling non-rigid shape matching. In this paper, we present a method for non-rigid, partial shape matching in vector graphics. Given a user-specified query region in a 2D shape, similar regions are found, even if they are non-linearly distorted. Furthermore, a non-linear mapping is established between the query regions and these matches, which allows the automatic transfer of editing operations such as texturing. This is achieved by a two-step approach. First, pointwise correspondences between the query region and the whole shape are established. The transformation parameters of these correspondences are registered in an appropriate transformation space. For transformations between similar regions, these parameters form surfaces in transformation space, which are extracted in the second step of our method. The extracted regions may be related to the query region by a non-rigid transform, enabling non-rigid shape matching.},
author = {Guerrero, Paul and Auzinger, Thomas and Wimmer, Michael and Jeschke, Stefan},
journal = {Computer Graphics Forum},
number = {1},
pages = {239 -- 252},
publisher = {Wiley},
title = {{Partial shape matching using transformation parameter similarity}},
doi = {10.1111/cgf.12509},
volume = {34},
year = {2014},
}
@article{1862,
abstract = {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.},
author = {Chen, Xu and Grandont, Laurie and Li, Hongjiang and Hauschild, Robert and Paque, Sébastien and Abuzeineh, Anas and Rakusová, Hana and Benková, Eva and Perrot Rechenmann, Catherine and Friml, Jirí},
journal = {Nature},
number = {729},
pages = {90 -- 93},
publisher = {Nature Publishing Group},
title = {{Inhibition of cell expansion by rapid ABP1-mediated auxin effect on microtubules}},
doi = {10.1038/nature13889},
volume = {516},
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{1870,
abstract = {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.},
author = {Henzinger, Thomas A and Otop, Jan and Samanta, Roopsha},
booktitle = {Leibniz International Proceedings in Informatics, LIPIcs},
location = {Delhi, India},
pages = {431 -- 443},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Lipschitz robustness of finite-state transducers}},
doi = {10.4230/LIPIcs.FSTTCS.2014.431},
volume = {29},
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},
}