The last few years have seen a resurgence of interest in the use of symbolic execution--program analysis technique developed more than three decades ago to analyze program execution paths. However, symbolic execution remains an expensive technique and scaling it remains a key technical challenge. There are two key factors that contribute to its cost: (1) the number of paths that need to be explored and (2) the cost of constraint solving, which is typically required for each path explored. Our insight is that the cost of symbolic execution can be reduced by an incremental approach, which uses static analysis and dynamic analysis to focus on relevant parts of code and reuse previous analysis results, thereby addressing both the key cost factors of symbolic execution. This dissertation presents Memoized Incremental Symbolic Execution, a novel approach that embodies our insight. Using symbolic execution in practice often requires several successive runs of the technique on largely similar underlying problems where successive problems differ due to some change, which may be to code, e.g., to fix a bug, to analysis parameters, e.g., to increase the path exploration depth, or to correctness properties, e.g., to check against stronger specifications that are written as assertions in code. Memoized Incremental Symbolic Execution, a three-fold approach, leverages the similarities in the successive problems to reduce the total cost of applying the technique. Our prototype tool-set is based on the Symbolic PathFinder. Experimental results show that Memoized Incremental Symbolic Execution enhances the efficacy of symbolic execution. / text

Yes / Background: stable isotope ratios of carbon (δ13C) and nitrogen (δ15N) in bone and dentine collagen have been used for over 30 years to estimate palaeodiet, subsistence strategy, breastfeeding duration and migration within burial populations. Recent developments in dentine microsampling allow improved temporal resolution for dietary patterns. Aim: We propose a simple method which could be applied to human teeth to estimate chronological age represented by dentine microsamples in the direction of tooth growth, allowing comparison of dietary patterns between individuals and populations. The method is tested using profiles from permanent and deciduous teeth of two individuals. Subjects and methods: using a diagrammatic representation of dentine development by approximate age for each human tooth (based on the Queen Mary University of London Atlas) (AlQahtani et al., 2010), we estimate the age represented by each dentine section. Two case studies are shown: comparison of M1 and M2 from a 19th century individual from London, England, and identification of an unknown tooth from an Iron Age female adult from Scotland. Results and conclusions: The isotopic profiles demonstrate that variations in consecutively-forming teeth can be aligned using this method to extend the dietary history of an individual, or identify an unknown tooth by matching the profiles.

Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.