| 1. |
- Almstedt, Karin, 1980-, et al.
(författare)
-
Unfolding a folding disease: folding, misfolding and aggregation of the marble brain syndrome-associated mutant H107Y of human carbonic anhydrase II
- 2004
-
Ingår i: Journal of Molecular Biology. - Oxford : Elsevier. - 0022-2836 .- 1089-8638. ; 342:2, s. 619-633
-
Tidskriftsartikel (refereegranskat)abstract
- Most loss-of-function diseases are caused by aberrant folding of important proteins. These proteins often misfold due to mutations. The disease marble brain syndrome (MBS), known also as carbonic anhydrase II deficiency syndrome (CADS), can manifest in carriers of point mutations in the human carbonic anhydrase II (HCA II) gene. One mutation associated with MBS entails the His107Tyr substitution. Here, we demonstrate that this mutation is a remarkably destabilizing folding mutation. The loss-of-function is clearly a folding defect, since the mutant shows 64% of CO2 hydration activity compared to that of the wild-type at low temperature where the mutant is folded. On the contrary, its stability towards thermal and guanidine hydrochloride (GuHCl) denaturation is highly compromised. Using activity assays, CD, fluorescence, NMR, cross-linking, aggregation measurements and molecular modeling, we have mapped the properties of this remarkable mutant. Loss of enzymatic activity had a midpoint temperature of denaturation (Tm) of 16 °C for the mutant compared to 55 °C for the wild-type protein. GuHCl-denaturation (at 4 °C) showed that the native state of the mutant was destabilized by 9.2 kcal/mol. The mutant unfolds through at least two equilibrium intermediates; one novel intermediate that we have termed the molten globule light state and, after further denaturation, the classical molten globule state is populated. Under physiological conditions (neutral pH; 37 °C), the His107Tyr mutant will populate the molten globule light state, likely due to novel interactions between Tyr107 and the surroundings of the critical residue Ser29 that destabilize the native conformation. This intermediate binds the hydrophobic dye 8-anilino-1-naphthalene sulfonic acid (ANS) but not as strong as the molten globule state, and near-UV CD reveals the presence of significant tertiary structure. Notably, this intermediate is not as prone to aggregation as the classical molten globule. As a proof of concept for an intervention strategy with small molecules, we showed that binding of the CA inhibitor acetazolamide increases the stability of the native state of the mutant by 2.9 kcal/mol in accordance with its strong affinity. Acetazolamide shifts the Tm to 34 °C that protects from misfolding and will enable a substantial fraction of the enzyme pool to survive physiological conditions.
|
|
| 2. |
|
|
| 3. |
- Glimelius, Bengt, et al.
(författare)
-
U-CAN : a prospective longitudinal collection of biomaterials and clinical information from adult cancer patients in Sweden.
- 2018
-
Ingår i: Acta Oncologica. - : Taylor & Francis. - 0284-186X .- 1651-226X. ; 57:2, s. 187-194
-
Tidskriftsartikel (refereegranskat)abstract
- Background: Progress in cancer biomarker discovery is dependent on access to high-quality biological materials and high-resolution clinical data from the same cases. To overcome current limitations, a systematic prospective longitudinal sampling of multidisciplinary clinical data, blood and tissue from cancer patients was therefore initiated in 2010 by Uppsala and Umeå Universities and involving their corresponding University Hospitals, which are referral centers for one third of the Swedish population.Material and Methods: Patients with cancer of selected types who are treated at one of the participating hospitals are eligible for inclusion. The healthcare-integrated sampling scheme encompasses clinical data, questionnaires, blood, fresh frozen and formalin-fixed paraffin-embedded tissue specimens, diagnostic slides and radiology bioimaging data.Results: In this ongoing effort, 12,265 patients with brain tumors, breast cancers, colorectal cancers, gynecological cancers, hematological malignancies, lung cancers, neuroendocrine tumors or prostate cancers have been included until the end of 2016. From the 6914 patients included during the first five years, 98% were sampled for blood at diagnosis, 83% had paraffin-embedded and 58% had fresh frozen tissues collected. For Uppsala County, 55% of all cancer patients were included in the cohort.Conclusions: Close collaboration between participating hospitals and universities enabled prospective, longitudinal biobanking of blood and tissues and collection of multidisciplinary clinical data from cancer patients in the U-CAN cohort. Here, we summarize the first five years of operations, present U-CAN as a highly valuable cohort that will contribute to enhanced cancer research and describe the procedures to access samples and data.
|
|
| 4. |
- Gustavsson, Anders, et al.
(författare)
-
Corrigendum to “Cost of disorders of the brain in Europe 2010” [Eur. Neuropsychopharmacol. 21 (2011) 718–779]
- 2012
-
Ingår i: European Neuropsychopharmacology. - : Elsevier BV. - 0924-977X .- 1873-7862. ; 22:3, s. 237-238
-
Tidskriftsartikel (refereegranskat)abstract
- The spectrum of disorders of the brain is large, covering hundreds of disorders that are listed in either the mental or neurological disorder chapters of the established international diagnostic classification systems. These disorders have a high prevalence as well as short- and long-term impairments and disabilities. Therefore they are an emotional, financial and social burden to the patients, their families and their social network. In a 2005 landmark study, we estimated for the first time the annual cost of 12 major groups of disorders of the brain in Europe and gave a conservative estimate of €386 billion for the year 2004. This estimate was limited in scope and conservative due to the lack of sufficiently comprehensive epidemiological and/or economic data on several important diagnostic groups. We are now in a position to substantially improve and revise the 2004 estimates. In the present report we cover 19 major groups of disorders, 7 more than previously, of an increased range of age groups and more cost items. We therefore present much improved cost estimates. Our revised estimates also now include the new EU member states, and hence a population of 514 million people.
|
|
| 5. |
- Thorgeirsson, Thorgeir E, et al.
(författare)
-
A variant associated with nicotine dependence, lung cancer and peripheral arterial disease
- 2008
-
Ingår i: Nature. - : Springer Science and Business Media LLC. - 0028-0836 .- 1476-4687. ; 452:7187, s. 9-638
-
Tidskriftsartikel (refereegranskat)abstract
- Smoking is a leading cause of preventable death, causing about 5 million premature deaths worldwide each year(1,2). Evidence for genetic influence on smoking behaviour and nicotine dependence (ND)(3-8) has prompted a search for susceptibility genes. Furthermore, assessing the impact of sequence variants on smoking-related diseases is important to public health(9,10). Smoking is the major risk factor for lung cancer (LC)(11-14) and is one of the main risk factors for peripheral arterial disease (PAD)(15-17). Here we identify a common variant in the nicotinic acetylcholine receptor gene cluster on chromosome 15q24 with an effect on smoking quantity, ND and the risk of two smoking- related diseases in populations of European descent. The variant has an effect on the number of cigarettes smoked per day in our sample of smokers. The same variant was associated with ND in a previous genomewide association study that used low- quantity smokers as controls(18,19), and with a similar approach we observe a highly significant association with ND. A comparison of cases of LC and PAD with population controls each showed that the variant confers risk of LC and PAD. The findings provide a case study of a gene - environment interaction(20), highlighting the role of nicotine addiction in the pathology of other serious diseases.
|
|
| 6. |
- Wahlin, Bengt, et al.
(författare)
-
Coronary Artery Calcification Is Related to Inflammation in Rheumatoid Arthritis : A Long-Term Follow-Up Study
- 2016
-
Ingår i: BioMed Research International. - : Hindawi Limited. - 2314-6133 .- 2314-6141.
-
Tidskriftsartikel (refereegranskat)abstract
- Objective. A long-term follow-up of patients with rheumatoid arthritis (RA) to evaluate factors related to coronary artery calcification (CAC). Methods. All 22 eligible patients (4 males/18 females, mean age 65 years, and RA-duration 30-36 years) from the original (baseline; n = 39) study of atherosclerosis were included. Inflammation, cardiovascular risk factors, and biomarkers were measured at baseline. At follow-up 13 years later, CAC was assessed by computed tomography (CT) and the grade of inflammation was measured. Multivariate analysis of differences between patients with low (0-10) and high CAC (>10) was done by orthogonal projection to latent structures (OPLS). Results. Ten patients had CAC 0-10 and 12 had >10 (range 18-1700). Patients with high CAC had significantly higher ESR (24.3 versus 9.9 mm/h) and swollen joint count (2 versus 0). The OPLS models discriminated between patients having high or low CAC. With only baseline variables, the sensitivity was 73% and the specificity 82%. The model that also included inflammatory variables from follow-up had a sensitivity of 89% and a specificity of 85%. Exclusion of baseline intima media thickness and plaque from the latter model modestly reduced the accuracy (sensitivity 80% and specificity 83%). Conclusions. CAC is related to inflammation in patients with RA.
|
|
| 7. |
|
|
| 8. |
- Zhang, Wei
(författare)
-
Directed Evolution of Glutathione Transferases with Altered Substrate Selectivity Profiles : A Laboratory Evolution Study Shedding Light on the Multidimensional Nature of Epistasis
- 2011
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Directed evolution is generally regarded as a useful approach in protein engineering. By subjecting members of a mutant library to the power of Darwinian evolution, desired protein properties are obtained. Numerous reports have appeared in the literature showing the success of tailoring proteins for various applications by this method. Is it a one-way track that protein practitioners can only learn from nature to enable more efficient protein engineering? A structure-and-mechanism-based approach, supplemented with the use of reduced amino acid alphabets, was proposed as a general means for semi-rational enzyme engineering. Using human GST A2-2*E, the most active human enzyme in the bioactivation of azathioprine, as a parental enzyme to test this approach, a L107G/L108D/F222H triple-point mutant of GST A2-2*E (thereafter designated as GDH) was discovered with 70-fold increased activity, approaching the upper limit of specific activity of the GST scaffold. The approach was further experimentally verified to be more successful than intuitively choosing active-site residues in proximity to the bound substrate for the improvement of enzyme performance. By constructing all intermediates along all putative mutational paths leading from GST A2-2*E to mutant GDH and assaying them with nine alternative substrates, the fitness landscapes were found to be “rugged” in differential fashions in substrate-activity space. The multidimensional fitness landscapes stemming from functional promiscuity can lead to alternative outcomes with enzymes optimized for other features than the selectable markers that were relevant at the origin of the evolutionary process. The results in this thesis suggest that in this manner an evolutionary response to changing environmental conditions can readily be mounted. In summary, the thesis demonstrates the attractive features of the structure-and-mechanism-based semi-rational directed evolution approach for optimizing enzyme performance. Moreover, the results gained from the studies show that laboratory evolution may refine our understanding of evolutionary process in nature.
|
|
| 9. |
|
|
| 10. |
|
|
| 11. |
- Aarts, Fides, et al.
(författare)
-
Generating models of infinite-state communication protocols using regular inference with abstraction
- 2015
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 46:1, s. 1-41
-
Tidskriftsartikel (refereegranskat)abstract
- In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.
|
|
| 12. |
|
|
| 13. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
A general approach to partial order reductions in symbolic verification
- 1998
-
Ingår i: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 379-390
-
Konferensbidrag (refereegranskat)abstract
- The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.
|
|
| 14. |
|
|
| 15. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Algorithmic Improvements in Regular Model Checking
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems, whose states can be represented as finite strings of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. In earlier papers, we have developed methods for computing the transitive closure (or the set of reachable states) of the transition relation, represented by a regular length-preserving transducer. In this paper, we present several improvements of these techniques, which reduce the size of intermediate approximations of the transitive closure: One improvement is to pre-process the transducer by \em bi-determinization, another is to use a more powerful equivalence relation for identifying histories (columns) of states in the transitive closure. We also present a simplified theoretical framework for showing soundness of the optimization, which is based on commuting simulations. The techniques have been implemented, and we report the speedups obtained from the respective optimizations.
|
|
| 16. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- 2013
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg.
-
Konferensbidrag (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependen- cies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded num- ber of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state au- tomata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verifica- tion, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have imple- mented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 17. |
|
|
| 18. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(författare)
-
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
- 2019
-
Ingår i: Networked Systems. - Cham : Springer Nature. - 9783030312770 - 9783030312763 ; , s. 3-18
-
Konferensbidrag (refereegranskat)abstract
- We describe at a high-level the main concepts in the Release-Acquire (RA) semantics that is part of the C11 language. Furthermore, we describe the ideas behind an optimal dynamic partial order reduction technique that can be used for systematic analysis of concurrent programs running under RA. This tutorial is based on the material presented in [5], which also contains the formal definitions of all the models, concepts, and algorithms.
|
|
| 19. |
|
|
| 20. |
|
|
| 21. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
On-the-fly analysis of systems with unbounded, lossy FIFO channels
- 1998
-
Ingår i: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 305-318
-
Konferensbidrag (refereegranskat)abstract
- We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
|
|
| 22. |
|
|
| 23. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Regular Model Checking for LTL(MSO)
- 2004
-
Ingår i: Proc. 16th Int. Conf. on Computer Aided Verification, LNCS.
-
Tidskriftsartikel (refereegranskat)
|
|
| 24. |
|
|
| 25. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Regular Tree Model Checking
- 2002
-
Ingår i: CAV 2002, 14th Int. Conf. on Computer Aided Verification.. ; , s. 555-568
-
Konferensbidrag (refereegranskat)
|
|
| 26. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for POWER
- 2016
-
Ingår i: Computer Aided Verification. - Cham : Springer. - 9783319415390 - 9783319415406 ; , s. 134-156
-
Konferensbidrag (refereegranskat)abstract
- We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.
|
|
| 27. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2015
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783662466803 ; , s. 353-367
-
Konferensbidrag (refereegranskat)
|
|
| 28. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2017
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 54:8, s. 789-818
-
Tidskriftsartikel (refereegranskat)
|
|
| 29. |
- Abdulla, Parosh, et al.
(författare)
-
A Survey of Regular Model Checking.
- 2004
-
Ingår i: CONCUR 2004 - Concurrency Theory. - 354022940X ; , s. 35-48
-
Konferensbidrag (refereegranskat)abstract
- Regular model checking is being developed for algorithmic verification of several classes of infinite-state systems whose configurations can be modeled as words over a finite alphabet. Examples include parameterized systems consisting of an arbitrary number of homogeneous finite-state processes connected in a linear or ring-formed topology, and systems that operate on queues, stacks, integers, and other linear data structures. The main idea is to use regular languages as the representation of sets of configurations, and finite-state transducers to describe transition relations. In general, the verification problems considered are all undecidable, so the work has consisted in developing semi-algorithms, and decidability results for restricted cases. This paper provides a survey of the work that has been performed so far, and some of its applications.
|
|
| 30. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Undecidable verification problems for programs with unreliable channels
- 1996
-
Ingår i: Automata, Languages and Programming. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540582014 - 9783540485667 ; , s. 71-90
-
Konferensbidrag (refereegranskat)abstract
- We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namelyThe model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.The results are obtained through a reduction from a variant of Post's Correspondence Problem.
|
|
| 31. |
|
|
| 32. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verification of heap manipulating programs with ordered data by extended forest automata
- 2016
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 53:4, s. 357-385
-
Tidskriftsartikel (refereegranskat)abstract
- We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.
|
|
| 33. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verifying networks of timed processes
- 1998
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - 9783540643562 - 9783540697534 ; , s. 298-312
-
Konferensbidrag (refereegranskat)abstract
- Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz. real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.
|
|
| 34. |
|
|
| 35. |
- Abdulla, Parosh, 1961-, et al.
(författare)
-
An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 19:5, s. 549-563
-
Tidskriftsartikel (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 36. |
- Abdulla, Parosh, et al.
(författare)
-
Automated Verification of Linearization Policies
- 2016
-
Ingår i: Automated Verification of Linearization Policies. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783662534120 - 9783662534137
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.
|
|
| 37. |
- Abdulla, Parosh, et al.
(författare)
-
Comparing source sets and persistent sets for partial order reduction
- 2017
-
Ingår i: Models, Algorithms, Logics and Tools. - Cham : Springer. - 9783319631202 - 9783319631219 ; , s. 516-536
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Partial order reduction has traditionally been based on persistent sets, ample sets, stubborn sets, or variants thereof. Recently, we have presented a strengthening of this foundation, using source sets instead of persistent/ample/stubborn sets. Source sets subsume persistent sets and are often smaller than persistent sets. We introduced source sets as a basis for Dynamic Partial Order Reduction (DPOR), in a framework which assumes that processes are deterministic and that all program executions are finite. In this paper, show how to use source sets for partial order reduction in a framework which does not impose these restrictions. We also compare source sets with persistent sets, providing some insights into conditions under which source sets and persistent sets do or do not differ.
|
|
| 38. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Consistency and Persistency in Program Verification : Challenges and Opportunities
- 2022
-
Ingår i: Principles of Systems Design. - Cham : Springer. - 9783031223365 - 9783031223372 ; , s. 494-510
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- We consider the verification of concurrent programs and, in particular, the challenges that arise because modern platforms only guarantee weak semantics, i.e., semantics that are weaker than the classical Sequential Consistency (SC). We describe two architectural concepts that give rise to weak semantics, namely weak consistency and weak persistency. The former defines the order in which operations issued by a given process become visible to the rest of the processes. The latter prescribes the order in which data becomes persistent. To deal with the extra complexity in program behaviors that arises due to weak semantics, we propose translating the program verification problem under weak semantics to SC. The main principle is to augment the program with a set of (unbounded) data structures that guarantee the equivalence of the source program’s behavior under the weak semantics with the augmented program’s behavior under the SC semantics. Such an equivalence opens the door to leverage, albeit in a non-trivial manner, the rich set of techniques that we have developed over the years for program verification under the SC semantics. We illustrate the framework’s potential by considering the persistent version of the well-known Total Store Order semantics. We show that we can capture the program behaviors on such a platform using a finite set of unbounded monotone FIFO buffers. The use of monotone FIFO buffers allows the use of the well-structured-systems framework to prove the decidability of the reachability problem.
|
|
| 39. |
|
|
| 40. |
- Abdulla, Parosh, et al.
(författare)
-
Optimal dynamic partial order reduction
- 2014
-
Ingår i: Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. - New York : ACM Press. - 9781450325448 ; , s. 373-384
-
Konferensbidrag (refereegranskat)abstract
- Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.
|
|
| 41. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Optimal stateless model checking for reads-from equivalence under sequential consistency
- 2019
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421.
-
Tidskriftsartikel (refereegranskat)abstract
- We present a new approach for stateless model checking (SMC) of multithreaded programs under Sequential Consistency (SC) semantics. To combat state-space explosion, SMC is often equipped with a partial-order reduction technique, which defines an equivalence on executions, and only needs to explore one execution in each equivalence class. Recently, it has been observed that the commonly used equivalence of Mazurkiewicz traces can be coarsened but still cover all program crashes and assertion violations. However, for this coarser equivalence, which preserves only the reads-from relation from writes to reads, there is no SMC algorithm which is (i) optimal in the sense that it explores precisely one execution in each reads-from equivalence class, and (ii) efficient in the sense that it spends polynomial effort per class. \end{inparaenum} We present the first SMC algorithm for SC that is both optimal and efficient in practice, meaning that it spends polynomial time per equivalence class on all programs that we have tried. This is achieved by a novel test that checks whether a given reads-from relation can arise in some execution. Our experimental results show that Nidhugg/rfsc, although slower than the fastest SMC tools in programs where tools happen to examine the same number of executions, always scales similarly or better than them, and outperforms them by an exponential factor in programs where the reads-from equivalence is coarser than the standard one. We also present two non-trivial use cases where the new equivalence is particularly effective, as well as the significant performance advantage that Nidhugg/rfsc offers compared to state-of-the-art SMC and systematic concurrency testing tools.
|
|
| 42. |
- Abdulla, Parosh, 1961-, et al.
(författare)
-
Optimal Stateless Model Checking under the Release-Acquire Semantics
- 2018
-
Ingår i: SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018. - : ACM Digital Library.
-
Konferensbidrag (refereegranskat)abstract
- We present a framework for efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which define how reads obtain their values from writes. This is in contrast to previous approaches, which in addition explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially large source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.
|
|
| 43. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Optimal Stateless Model Checking under the Release-Acquire Semantics
- 2018
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 2:OOPSLA, s. 1-29
-
Tidskriftsartikel (refereegranskat)abstract
- We present a framework for the efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which specify how reads obtain their values from writes. This is in contrast to previous approaches, which also explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially significant source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.
|
|
| 44. |
- Abdulla, Parosh, et al.
(författare)
-
Regular Model Checking for LTL(MSO)
- 2004
-
Ingår i: Computer Aided Verification. - 3540223428 ; , s. 348-360
-
Konferensbidrag (refereegranskat)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present $\logic$, a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. $\logic$ is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process.We give a technique for model checking $\logic$, which is adapted from the automata-theoretic approach: a formula is translated to a (\buchi) transducer with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique and show its application to a number of parameterized algorithms from the literature.
|
|
| 45. |
- Abdulla, Parosh, et al.
(författare)
-
Regular model checking for LTL(MSO)
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - Springer : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 223-241
-
Tidskriftsartikel (refereegranskat)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a Buechi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature.
|
|
| 46. |
|
|
| 47. |
|
|
| 48. |
- Abdulla, Parosh, 1961-, et al.
(författare)
-
Source Sets : A Foundation for Optimal Dynamic Partial Order Reduction
- 2017
-
Ingår i: Journal of the ACM. - : Association for Computing Machinery (ACM). - 0004-5411 .- 1557-735X. ; 64:4
-
Tidskriftsartikel (refereegranskat)abstract
- Stateless model checking is a powerful method for program verification that, however, suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, we present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, that replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple-to-implement algorithm, called source-DPOR. Subsequently, we enhance this algorithm with a novel mechanism, called wakeup trees, that allows the resulting algorithm, called optimal-DPOR, to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, for example, via locks. Finally, we discuss tradeoffs of the source-and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs, while the source-DPOR algorithm is at the core of a publicly available stateless model checking tool for C/pthread programs running on machines with relaxed memory models. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.
|
|
| 49. |
|
|
| 50. |
|
|
