| 1. |
|
|
| 2. |
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Monotonic abstraction for programs with dynamic memory heaps
- 2008
-
Ingår i: Computer Aided Verification. - Berlin : Springer-Verlag. ; , s. 341-354
-
Konferensbidrag (refereegranskat)abstract
- We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach.
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Monotonic abstraction for programs with multiply-linked structures
- 2013
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 24:2, s. 187-210
-
Tidskriftsartikel (refereegranskat)abstract
- We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.
|
|
| 5. |
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Timed lossy channel systems
- 2012
-
Ingår i: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783939897477 ; , s. 374-386
-
Konferensbidrag (refereegranskat)
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Timed Lossy Channel Systems
- 2012
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Lossy channel systems are a classical model with applications ranging from the modeling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this paper, we extend the model by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of \emphTimed Lossy Channel Systems (TLCS). The main contribution of the paper is to show that the control state reachability problem is decidable for TLCS.
|
|
| 8. |
- Ji, Ran, 1982, et al.
(författare)
-
Automated Analysis of Data-Dependent Programs with Dynamic Memory
- 2009
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - : Department of Information Technology, Uppsala University. - 1611-3349 .- 0302-9743. - 9783642047602 ; 5799:Lecture Notes in Computer Science, s. 197-212
-
Konferensbidrag (refereegranskat)abstract
- We present a new approach for automatic verification of data-dependent programs manipulating dynamic heaps. A heap is encoded by a graph where the nodes represent the cells, and the edges reflect the pointer structure between the cells of the heap. Each cell contains a set of variables which range over the natural numbers. Our method relies on standard backward reachability analysis, where the main idea is to use a simple set of predicates, called signatures, in order to represent bad sets of heaps. Examples of bad heaps are those which contain either garbage, lists which are not well-formed, or lists which are not sorted. We present the results for the case of programs with a single next-selector, and where variables may be compared for (in)equality. This allows us to verify for instance that a program, like bubble sort or insertion sort, returns a list which is well-formed and sorted, or that the merging of two sorted lists is a new sorted list. We report on the result of running a prototype based on the method on a number of programs.
|
|
| 9. |
- Mohammad, Moman A., et al.
(författare)
-
Christmas, national holidays, sport events, and time factors as triggers of acute myocardial infarction : SWEDEHEART observational study 1998-2013
- 2018
-
Ingår i: The BMJ. - : BMJ Publishing Group Ltd. - 1756-1833 .- 0959-8138. ; 363
-
Tidskriftsartikel (refereegranskat)abstract
- OBJECTIVES: To study circadian rhythm aspects, national holidays, and major sports events as triggers of myocardial infarction.DESIGN: Retrospective observational study using the nationwide coronary care unit registry, SWEDEHEART.SETTING: Sweden.PARTICIPANTS: 283 014 cases of myocardial infarction reported to SWEDEHEART between 1998 and 2013. Symptom onset date was documented for all cases, and time to the nearest minute for 88%.INTERVENTIONS: Myocardial infarctions with symptom onset on Christmas/New Year, Easter, and Midsummer holiday were identified. Similarly, myocardial infarctions that occurred during a FIFA World Cup, UEFA European Championship, and winter and summer Olympic Games were identified. The two weeks before and after a holiday were set as a control period, and for sports events the control period was set to the same time one year before and after the tournament. Circadian and circaseptan analyses were performed with Sunday and 24:00 as the reference day and hour with which all other days and hours were compared. Incidence rate ratios were calculated using a count regression model.MAIN OUTCOME MEASURES: Daily count of myocardial infarction.RESULTS: Christmas and Midsummer holidays were associated with a higher risk of myocardial infarction (incidence rate ratio 1.15, 95% confidence interval 1.12 to 1.19, P<0.001, and 1.12, 1.07 to 1.18, P<0.001, respectively). The highest associated risk was observed for Christmas Eve (1.37, 1.29 to 1.46, P<0.001). No increased risk was observed during Easter holiday or sports events. A circaseptan and circadian variation in the risk of myocardial infarction was observed, with higher risk during early mornings and on Mondays. Results were more pronounced in patients aged over 75 and those with diabetes and a history of coronary artery disease.CONCLUSIONS: In this nationwide real world study covering 16 years of hospital admissions for myocardial infarction with symptom onset documented to the nearest minute, Christmas, and Midsummer holidays were associated with higher risk of myocardial infarction, particularly in older and sicker patients, suggesting a role of external triggers in vulnerable individuals.
|
|
