@article{1202,
author = {Milutinovic, Barbara and Peuß, Robert and Ferro, Kevin and Kurtz, Joachim},
journal = {Zoology },
number = {4},
pages = {254 -- 261},
publisher = {Elsevier},
title = {{Immune priming in arthropods: an update focusing on the red flour beetle}},
doi = {10.1016/j.zool.2016.03.006},
volume = {119},
year = {2016},
}
@article{1203,
abstract = {Haemophilus haemolyticus has been recently discovered to have the potential to cause invasive disease. It is closely related to nontypeable Haemophilus influenzae (NT H. influenzae). NT H. influenzae and H. haemolyticus are often misidentified because none of the existing tests targeting the known phenotypes of H. haemolyticus are able to specifically identify H. haemolyticus. Through comparative genomic analysis of H. haemolyticus and NT H. influenzae, we identified genes unique to H. haemolyticus that can be used as targets for the identification of H. haemolyticus. A real-time PCR targeting purT (encoding phosphoribosylglycinamide formyltransferase 2 in the purine synthesis pathway) was developed and evaluated. The lower limit of detection was 40 genomes/PCR; the sensitivity and specificity in detecting H. haemolyticus were 98.9% and 97%, respectively. To improve the discrimination of H. haemolyticus and NT H. influenzae, a testing scheme combining two targets (H. haemolyticus purT and H. influenzae hpd, encoding protein D lipoprotein) was also evaluated and showed 96.7% sensitivity and 98.2% specificity for the identification of H. haemolyticus and 92.8% sensitivity and 100% specificity for the identification of H. influenzae, respectively. The dual-target testing scheme can be used for the diagnosis and surveillance of infection and disease caused by H. haemolyticus and NT H. influenzae.},
author = {Hu, Fang and Rishishwar, Lavanya and Sivadas, Ambily and Mitchell, Gabriel and King, Jordan and Murphy, Timothy and Gilsdorf, Janet and Mayer, Leonard and Wang, Xin},
journal = {Journal of Clinical Microbiology},
number = {12},
pages = {3010 -- 3017},
publisher = {American Society for Microbiology},
title = {{Comparative genomic analysis of Haemophilus haemolyticus and nontypeable Haemophilus influenzae and a new testing scheme for their discrimination}},
doi = {10.1128/JCM.01511-16},
volume = {54},
year = {2016},
}
@article{1204,
abstract = {In science, as in life, "surprises" can be adequately appreciated only in the presence of a null model, what we expect a priori. In physics, theories sometimes express the values of dimensionless physical constants as combinations of mathematical constants like π or e. The inverse problem also arises, whereby the measured value of a physical constant admits a "surprisingly" simple approximation in terms of well-known mathematical constants. Can we estimate the probability for this to be a mere coincidence, rather than an inkling of some theory? We answer the question in the most naive form.},
author = {Amir, Ariel and Lemeshko, Mikhail and Tokieda, Tadashi},
journal = {American Mathematical Monthly},
number = {6},
pages = {609 -- 612},
publisher = {Mathematical Association of America},
title = {{Surprises in numerical expressions of physical constants}},
doi = {10.4169/amer.math.monthly.123.6.609},
volume = {123},
year = {2016},
}
@inproceedings{1205,
abstract = {In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.},
author = {Jiang, Yu and Liu, Han and Song, Houbing and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui},
location = {Limassol, Cyprus},
pages = {757 -- 763},
publisher = {Springer},
title = {{Safety assured formal model driven design of the multifunction vehicle bus controller}},
doi = {10.1007/978-3-319-48989-6_47},
volume = {9995},
year = {2016},
}
@article{1206,
abstract = {We study a polar molecule immersed in a superfluid environment, such as a helium nanodroplet or a Bose–Einstein condensate, in the presence of a strong electrostatic field. We show that coupling of the molecular pendular motion, induced by the field, to the fluctuating bath leads to formation of pendulons—spherical harmonic librators dressed by a field of many-particle excitations. We study the behavior of the pendulon in a broad range of molecule–bath and molecule–field interaction strengths, and reveal that its spectrum features a series of instabilities which are absent in the field-free case of the angulon quasiparticle. Furthermore, we show that an external field allows to fine-tune the positions of these instabilities in the molecular rotational spectrum. This opens the door to detailed experimental studies of redistribution of orbital angular momentum in many-particle systems. © 2016 Wiley-VCH Verlag GmbH & Co. KGaA, Weinheim},
author = {Redchenko, Elena and Lemeshko, Mikhail},
journal = {ChemPhysChem},
number = {22},
pages = {3649 -- 3654},
publisher = {Wiley-Blackwell},
title = {{Libration of strongly oriented polar molecules inside a superfluid}},
doi = {10.1002/cphc.201601042},
volume = {17},
year = {2016},
}
@article{1209,
abstract = {NADH-ubiquinone oxidoreductase (complex I) is the largest (∼1 MDa) and the least characterized complex of the mitochondrial electron transport chain. Because of the ease of sample availability, previous work has focused almost exclusively on bovine complex I. However, only medium resolution structural analyses of this complex have been reported. Working with other mammalian complex I homologues is a potential approach for overcoming these limitations. Due to the inherent difficulty of expressing large membrane protein complexes, screening of complex I homologues is limited to large mammals reared for human consumption. The high sequence identity among these available sources may preclude the benefits of screening. Here, we report the characterization of complex I purified from Ovis aries (ovine) heart mitochondria. All 44 unique subunits of the intact complex were identified by mass spectrometry. We identified differences in the subunit composition of subcomplexes of ovine complex I as compared with bovine, suggesting differential stability of inter-subunit interactions within the complex. Furthermore, the 42-kDa subunit, which is easily lost from the bovine enzyme, remains tightly bound to ovine complex I. Additionally, we developed a novel purification protocol for highly active and stable mitochondrial complex I using the branched-chain detergent lauryl maltose neopentyl glycol. Our data demonstrate that, although closely related, significant differences exist between the biochemical properties of complex I prepared from ovine and bovine mitochondria and that ovine complex I represents a suitable alternative target for further structural studies. },
author = {Letts, James A and Degliesposti, Gianluca and Fiedorczuk, Karol and Skehel, Mark and Sazanov, Leonid A},
journal = {Journal of Biological Chemistry},
number = {47},
pages = {24657 -- 24675},
publisher = {American Society for Biochemistry and Molecular Biology},
title = {{Purification of ovine respiratory complex i results in a highly active and stable preparation}},
doi = {10.1074/jbc.M116.735142},
volume = {291},
year = {2016},
}
@article{1212,
abstract = {Plants adjust their growth according to gravity. Gravitropism involves gravity perception, signal transduction, and asymmetric growth response, with organ bending as a consequence [1]. Asymmetric growth results from the asymmetric distribution of the plant-specific signaling molecule auxin [2] that is generated by lateral transport, mediated in the hypocotyl predominantly by the auxin transporter PIN-FORMED3 (PIN3) [3–5]. Gravity stimulation polarizes PIN3 to the bottom sides of endodermal cells, correlating with increased auxin accumulation in adjacent tissues at the lower side of the stimulated organ, where auxin induces cell elongation and, hence, organ bending. A curvature response allows the hypocotyl to resume straight growth at a defined angle [6], implying that at some point auxin symmetry is restored to prevent overbending. Here, we present initial insights into cellular and molecular mechanisms that lead to the termination of the tropic response. We identified an auxin feedback on PIN3 polarization as underlying mechanism that restores symmetry of the PIN3-dependent auxin flow. Thus, two mechanistically distinct PIN3 polarization events redirect auxin fluxes at different time points of the gravity response: first, gravity-mediated redirection of PIN3-mediated auxin flow toward the lower hypocotyl side, where auxin gradually accumulates and promotes growth, and later PIN3 polarization to the opposite cell side, depleting this auxin maximum to end the bending. Accordingly, genetic or pharmacological interference with the late PIN3 polarization prevents termination of the response and leads to hypocotyl overbending. This observation reveals a role of auxin feedback on PIN polarity in the termination of the tropic response. © 2016 Elsevier Ltd},
author = {Rakusová, Hana and Abbas, Mohamad and Han, Huibin and Song, Siyuan and Robert, Hélène and Friml, Jirí},
journal = {Current Biology},
number = {22},
pages = {3026 -- 3032},
publisher = {Cell Press},
title = {{Termination of shoot gravitropic responses by auxin feedback on PIN3 polarity}},
doi = {10.1016/j.cub.2016.08.067},
volume = {26},
year = {2016},
}
@article{1216,
abstract = {A framework fo r extracting features in 2D transient flows, based on the acceleration field to ensure Galilean invariance is proposed in this paper. The minima of the acceleration magnitude (a superset of acceleration zeros) are extracted and discriminated into vortices and saddle points, based on the spectral properties of the velocity Jacobian. The extraction of topological features is performed with purely combinatorial algorithms from discrete computational topology. The feature points are prioritized with persistence, as a physically meaningful importance measure. These feature points are tracked in time with a robust algorithm for tracking features. Thus, a space-time hierarchy of the minima is built and vortex merging events are detected. We apply the acceleration feature extraction strategy to three two-dimensional shear flows: (1) an incompressible periodic cylinder wake, (2) an incompressible planar mixing layer and (3) a weakly compressible planar jet. The vortex-like acceleration feature points are shown to be well aligned with acceleration zeros, maxima of the vorticity magnitude, minima of the pressure field and minima of λ2.},
author = {Kasten, Jens and Reininghaus, Jan and Hotz, Ingrid and Hege, Hans and Noack, Bernd and Daviller, Guillaume and Morzyński, Marek},
journal = {Archives of Mechanics},
number = {1},
pages = {55 -- 80},
publisher = {Polish Academy of Sciences Publishing House},
title = {{Acceleration feature points of unsteady shear flows}},
volume = {68},
year = {2016},
}
@article{1218,
abstract = {Investigating the physiology of cyanobacteria cultured under a diel light regime is relevant for a better understanding of the resulting growth characteristics and for specific biotechnological applications that are foreseen for these photosynthetic organisms. Here, we present the results of a multiomics study of the model cyanobacterium Synechocystis sp. strain PCC 6803, cultured in a lab-scale photobioreactor in physiological conditions relevant for large-scale culturing. The culture was sparged withN2 andCO2, leading to an anoxic environment during the dark period. Growth followed the availability of light. Metabolite analysis performed with 1Hnuclear magnetic resonance analysis showed that amino acids involved in nitrogen and sulfur assimilation showed elevated levels in the light. Most protein levels, analyzed through mass spectrometry, remained rather stable. However, several high-light-response proteins and stress-response proteins showed distinct changes at the onset of the light period. Microarray-based transcript analysis found common patterns of~56% of the transcriptome following the diel regime. These oscillating transcripts could be grouped coarsely into genes that were upregulated and downregulated in the dark period. The accumulated glycogen was degraded in the anaerobic environment in the dark. A small part was degraded gradually, reflecting basic maintenance requirements of the cells in darkness. Surprisingly, the largest part was degraded rapidly in a short time span at the end of the dark period. This degradation could allow rapid formation of metabolic intermediates at the end of the dark period, preparing the cells for the resumption of growth at the start of the light period.},
author = {Angermayr, Andreas and Van Alphen, Pascal and Hasdemir, Dicle and Kramer, Gertjan and Iqbal, Muzamal and Van Grondelle, Wilmar and Hoefsloot, Huub and Choi, Younghae and Hellingwerf, Klaas},
journal = {Applied and Environmental Microbiology},
number = {14},
pages = {4180 -- 4189},
publisher = {American Society for Microbiology},
title = {{Culturing synechocystis sp. Strain pcc 6803 with N2 and CO2 in a diel regime reveals multiphase glycogen dynamics with low maintenance costs}},
doi = {10.1128/AEM.00256-16},
volume = {82},
year = {2016},
}
@article{1219,
abstract = {We consider N×N random matrices of the form H = W + V where W is a real symmetric or complex Hermitian Wigner matrix and V is a random or deterministic, real, diagonal matrix whose entries are independent of W. We assume subexponential decay for the matrix entries of W, and we choose V so that the eigenvalues ofW and V are typically of the same order. For a large class of diagonal matrices V , we show that the local statistics in the bulk of the spectrum are universal in the limit of large N.},
author = {Lee, Jioon and Schnelli, Kevin and Stetler, Ben and Yau, Horngtzer},
journal = {Annals of Probability},
number = {3},
pages = {2349 -- 2425},
publisher = {Institute of Mathematical Statistics},
title = {{Bulk universality for deformed wigner matrices}},
doi = {10.1214/15-AOP1023},
volume = {44},
year = {2016},
}
@article{122,
abstract = {Four rigid panels connected by hinges that meet at a point form a four-vertex, the fundamental building block of origami metamaterials. Most materials designed so far are based on the same four-vertex geometry, and little is known regarding how different geometries affect folding behavior. Here we systematically categorize and analyze the geometries and resulting folding motions of Euclidean four-vertices. Comparing the relative sizes of sector angles, we identify three types of generic vertices and two accompanying subtypes. We determine which folds can fully close and the possible mountain-valley assignments. Next, we consider what occurs when sector angles or sums thereof are set equal, which results in 16 special vertex types. One of these, flat-foldable vertices, has been studied extensively, but we show that a wide variety of qualitatively different folding motions exist for the other 15 special and 3 generic types. Our work establishes a straightforward set of rules for understanding the folding motion of both generic and special four-vertices and serves as a roadmap for designing origami metamaterials.},
author = {Waitukaitis, Scott R and Van Hecke, Martin},
journal = {Physical Review E - Statistical, Nonlinear, and Soft Matter Physics},
number = {2},
publisher = {American Physiological Society},
title = {{Origami building blocks: Generic and special four-vertices}},
doi = {10.1103/PhysRevE.93.023003},
volume = {93},
year = {2016},
}
@inproceedings{1220,
abstract = {Theoretical and numerical aspects of aerodynamic efficiency of propulsion systems coupled to the boundary layer of a fuselage are studied. We discuss the effects of local flow fields, which are affected both by conservative flow acceleration as well as total pressure losses, on the efficiency of boundary layer immersed propulsion devices. We introduce the concept of a boundary layer retardation turbine that helps reduce skin friction over the fuselage. We numerically investigate efficiency gains offered by boundary layer and wake interacting devices. We discuss the results in terms of a total energy consumption framework and show that efficiency gains of any device depend on all the other elements of the propulsion system.},
author = {Mikić, Gregor and Stoll, Alex and Bevirt, Joe and Grah, Rok and Moore, Mark},
location = {Washington, D.C., USA},
pages = {1 -- 19},
publisher = {AIAA},
title = {{Fuselage boundary layer ingestion propulsion applied to a thin haul commuter aircraft for optimal efficiency}},
doi = {10.2514/6.2016-3764},
year = {2016},
}
@article{1221,
abstract = {The Auxin Binding Protein 1 (ABP1) is one of the most studied proteins in plants. Since decades ago, it has been the prime receptor candidate for the plant hormone auxin with a plethora of described functions in auxin signaling and development. The developmental importance of ABP1 has recently been questioned by identification of Arabidopsis thaliana abp1 knock-out alleles that show no obvious phenotypes under normal growth conditions. In this study, we examined the contradiction between the normal growth and development of the abp1 knock-outs and the strong morphological defects observed in three different ethanol-inducible abp1 knock-down mutants ( abp1-AS, SS12K, SS12S). By analyzing segregating populations of abp1 knock-out vs. abp1 knock-down crosses we show that the strong morphological defects that were believed to be the result of conditional down-regulation of ABP1 can be reproduced also in the absence of the functional ABP1 protein. This data suggests that the phenotypes in abp1 knock-down lines are due to the off-target effects and asks for further reflections on the biological function of ABP1 or alternative explanations for the missing phenotypic defects in the abp1 loss-of-function alleles.},
author = {Michalko, Jaroslav and Glanc, Matous and Perrot Rechenmann, Catherine and Friml, Jirí},
journal = {F1000 Research },
publisher = {F1000 Research Ltd. },
title = {{Strong morphological defects in conditional Arabidopsis abp1 knock-down mutants generated in absence of functional ABP1 protein}},
doi = {10.12688/f1000research.7654.1},
volume = {5},
year = {2016},
}
@article{1222,
abstract = {We consider packings of congruent circles on a square flat torus, i.e., periodic (w.r.t. a square lattice) planar circle packings, with the maximal circle radius. This problem is interesting due to a practical reason—the problem of “super resolution of images.” We have found optimal arrangements for N=6, 7 and 8 circles. Surprisingly, for the case N=7 there are three different optimal arrangements. Our proof is based on a computer enumeration of toroidal irreducible contact graphs.},
author = {Musin, Oleg and Nikitenko, Anton},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {1 -- 20},
publisher = {Springer},
title = {{Optimal packings of congruent circles on a square flat torus}},
doi = {10.1007/s00454-015-9742-6},
volume = {55},
year = {2016},
}
@article{1223,
abstract = {We consider a random Schrödinger operator on the binary tree with a random potential which is the sum of a random radially symmetric potential, Qr, and a random transversally periodic potential, κQt, with coupling constant κ. Using a new one-dimensional dynamical systems approach combined with Jensen's inequality in hyperbolic space (our key estimate) we obtain a fractional moment estimate proving localization for small and large κ. Together with a previous result we therefore obtain a model with two Anderson transitions, from localization to delocalization and back to localization, when increasing κ. As a by-product we also have a partially new proof of one-dimensional Anderson localization at any disorder.},
author = {Froese, Richard and Lee, Darrick and Sadel, Christian and Spitzer, Wolfgang and Stolz, Günter},
journal = {Journal of Spectral Theory},
number = {3},
pages = {557 -- 600},
publisher = {European Mathematical Society},
title = {{Localization for transversally periodic random potentials on binary trees}},
doi = {10.4171/JST/132},
volume = {6},
year = {2016},
}
@inproceedings{1225,
abstract = {At Crypto 2015 Fuchsbauer, Hanser and Slamanig (FHS) presented the first standard-model construction of efficient roundoptimal blind signatures that does not require complexity leveraging. It is conceptually simple and builds on the primitive of structure-preserving signatures on equivalence classes (SPS-EQ). FHS prove the unforgeability of their scheme assuming EUF-CMA security of the SPS-EQ scheme and hardness of a version of the DH inversion problem. Blindness under adversarially chosen keys is proven under an interactive variant of the DDH assumption. We propose a variant of their scheme whose blindness can be proven under a non-interactive assumption, namely a variant of the bilinear DDH assumption. We moreover prove its unforgeability assuming only unforgeability of the underlying SPS-EQ but no additional assumptions as needed for the FHS scheme.},
author = {Fuchsbauer, Georg and Hanser, Christian and Kamath Hosdurg, Chethan and Slamanig, Daniel},
location = {Amalfi, Italy},
pages = {391 -- 408},
publisher = {Springer},
title = {{Practical round-optimal blind signatures in the standard model from weaker assumptions}},
doi = {10.1007/978-3-319-44618-9_21},
volume = {9841},
year = {2016},
}
@article{1226,
abstract = {Mitochondrial complex I (also known as NADH:ubiquinone oxidoreductase) contributes to cellular energy production by transferring electrons from NADH to ubiquinone coupled to proton translocation across the membrane. It is the largest protein assembly of the respiratory chain with a total mass of 970 kilodaltons. Here we present a nearly complete atomic structure of ovine (Ovis aries) mitochondrial complex I at 3.9 Å resolution, solved by cryo-electron microscopy with cross-linking and mass-spectrometry mapping experiments. All 14 conserved core subunits and 31 mitochondria-specific supernumerary subunits are resolved within the L-shaped molecule. The hydrophilic matrix arm comprises flavin mononucleotide and 8 iron-sulfur clusters involved in electron transfer, and the membrane arm contains 78 transmembrane helices, mostly contributed by antiporter-like subunits involved in proton translocation. Supernumerary subunits form an interlinked, stabilizing shell around the conserved core. Tightly bound lipids (including cardiolipins) further stabilize interactions between the hydrophobic subunits. Subunits with possible regulatory roles contain additional cofactors, NADPH and two phosphopantetheine molecules, which are shown to be involved in inter-subunit interactions. We observe two different conformations of the complex, which may be related to the conformationally driven coupling mechanism and to the active-deactive transition of the enzyme. Our structure provides insight into the mechanism, assembly, maturation and dysfunction of mitochondrial complex I, and allows detailed molecular analysis of disease-causing mutations.},
author = {Fiedorczuk, Karol and Letts, James A and Degliesposti, Gianluca and Kaszuba, Karol and Skehel, Mark and Sazanov, Leonid A},
journal = {Nature},
number = {7625},
pages = {406 -- 410},
publisher = {Nature Publishing Group},
title = {{Atomic structure of the entire mammalian mitochondrial complex i}},
doi = {10.1038/nature19794},
volume = {538},
year = {2016},
}
@inproceedings{1227,
abstract = {Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.},
author = {Kong, Hui and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu and Henzinger, Thomas A and Jiang, Yu and Schilling, Christian},
location = {Grenoble, France},
pages = {128 -- 144},
publisher = {Springer},
title = {{Discrete abstraction of multiaffine systems}},
doi = {10.1007/978-3-319-47151-8_9},
volume = {9957},
year = {2016},
}
@inproceedings{1229,
abstract = {Witness encryption (WE) was introduced by Garg et al. [GGSW13]. A WE scheme is defined for some NP language L and lets a sender encrypt messages relative to instances x. A ciphertext for x can be decrypted using w witnessing x ∈ L, but hides the message if x ∈ L. Garg et al. construct WE from multilinear maps and give another construction [GGH+13b] using indistinguishability obfuscation (iO) for circuits. Due to the reliance on such heavy tools, WE can cur- rently hardly be implemented on powerful hardware and will unlikely be realizable on constrained devices like smart cards any time soon. We construct a WE scheme where encryption is done by simply computing a Naor-Yung ciphertext (two CPA encryptions and a NIZK proof). To achieve this, our scheme has a setup phase, which outputs public parameters containing an obfuscated circuit (only required for decryption), two encryption keys and a common reference string (used for encryption). This setup need only be run once, and the parame- ters can be used for arbitrary many encryptions. Our scheme can also be turned into a functional WE scheme, where a message is encrypted w.r.t. a statement and a function f, and decryption with a witness w yields f (m, w). Our construction is inspired by the functional encryption scheme by Garg et al. and we prove (selective) security assuming iO and statistically simulation-sound NIZK. We give a construction of the latter in bilinear groups and combining it with ElGamal encryption, our ciphertexts are of size 1.3 kB at a 128-bit security level and can be computed on a smart card.},
author = {Abusalah, Hamza M and Fuchsbauer, Georg and Pietrzak, Krzysztof Z},
location = {Guildford, UK},
pages = {285 -- 303},
publisher = {Springer},
title = {{Offline witness encryption}},
doi = {10.1007/978-3-319-39555-5_16},
volume = {9696},
year = {2016},
}
@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},
}