| 31. |
|
|
| 32. |
|
|
| 33. |
- Abdulla, Aziz, et al.
(författare)
-
Monotonic Abstraction : on Efficient Verification of Parameterized Systems
- 2009
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:5, s. 779-801
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols
|
|
| 34. |
|
|
| 35. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Automatic verification of directory-based consistency protocols with graph constraints
- 2011
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 22:4, s. 761-782
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings.
|
|
| 36. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Counter-Example Guided Fence Insertion under TSO
- 2012
-
Ingår i: TACAS 2012. - Berlin, Heidelberg : Springer. - 9783642287558 - 9783642287565
-
Konferensbidrag (refereegranskat)abstract
- We give a sound and complete fence insertion procedure for concurrentfinite-state programs running under the classical TSO memory model. Thismodel allows “write to read” relaxation corresponding to the addition of an unboundedstore buffer between each processor and the main memory. We introducea novel machine model, called the Single-Buffer (SB) semantics, and show thatthe reachability problem for a program under TSO can be reduced to the reachabilityproblem under SB. We present a simple and effective backward reachabilityanalysis algorithm for the latter, and propose a counter-example guided fence insertionprocedure. The procedure is augmented by a placement constraint thatallows the user to choose places inside the program where fences may be inserted.For a given placement constraint, we automatically infer all minimal setsof fences that ensure correctness. We have implemented a prototype and run itsuccessfully on all standard benchmarks together with several challenging examplesthat are beyond the applicability of existing methods.
|
|
| 37. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
- 2013
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642367410 - 9783642367427 ; , s. 530-536
-
Konferensbidrag (refereegranskat)abstract
- We introduce MEMORAX, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the sizes of the store buffers could grow unboundedly, and hence the state spaces that need to be explored could be of infinite size. In addition, MEMORAX in- corporates an interpolation based CEGAR loop to make possible the verification of control state reachability for concurrent programs involving integer variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee the unreachability of bad control states under TSO. In fact, for programs only involving finite range variables and running on TSO, the fence insertion functionality is complete, i.e., it will find all minimal sets of memory fence placements (minimal in the sense that removing any fence would result in the reachability of the bad control states). This makes MEMORAX the first freely available, open source, push-button verification and fence insertion tool for programs running under TSO with integer variables.
|
|
| 38. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verifying Safety and Liveness for the FlexTM Hybrid Transactional Memory
- 2013
-
Ingår i: <em>Design, Automation & Test in Europe (DATE 2013), Grenoble, France, March 18-22, 2013.</em>. - Grenoble, France : IEEE. - 9781467350716 ; , s. 785-790
-
Konferensbidrag (refereegranskat)abstract
- We consider the verification of safety (strict se- rializability and abort consistency) and liveness (obstruction and livelock freedom) for the hybrid transactional memory framework FLEXTM. This framework allows for flexible imple- mentations of transactional memories based on an adaptation of the MESI coherence protocol. FLEXTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use the latest antichain based techniques to handle systems with tens of thousands of states.
|
|
| 39. |
- Abe, Y, et al.
(författare)
-
Feasibility of a nylon-mesh holder for vitrification of bovine germinal vesicle oocytes in subsequent production of viable blastocysts
- 2005
-
Ingår i: Biology of Reproduction. - : Society for the Study of Reproduction. - 0006-3363 .- 1529-7268. ; 72:6, s. 1416-1420
-
Tidskriftsartikel (refereegranskat)abstract
- To improve the feasibility of nylon-mesh holder for vitrification of bovine cumulus-oocytes complexes (GV-COCs) having germinal vesicle, this study was conducted to demonstrate effects of sugars and protocol of exposure in vitrification on subsequent in vitro maturation, ultrastructural changes, and in vitro development in bovine immature oocytes after cryopreservation using nylon mesh. Before vitrification, GV-COCs were exposed to the cryoprotectant, which was composed of 40% (v/v) ethylene glycol, 18% (w/v) Ficoll-70, and 0.3 M sucrose (EFS40) or 0.3 M trehalose (EFT40), either by single step or in a stepwise way. The maturation rates in the stepwise exposure with EFS40 or EFT40 were significantly higher (P less than 0.05) compared with the corresponding rates in the single step. In the stepwise exposure, few abnormalities were observed compared with the single-step exposure, where most oocytes showed a highly vacuolated cytoplasm with many ruptured mitochondria. Cleavage rates in fertilized oocytes previously exposed stepwise to EFS40 or EFT40 were significantly higher than those exposed by the single-step procedure. The cleaved embryos derived from the stepwise exposure to EFS40 developed to blastocysts. After transfer of blastocysts derived from vitrified GV oocytes, a female calf was born. These results indicate that vitrification of large numbers of bovine GV-COCs using a nylon-mesh holder accompanied with stepwise exposure minimizes structural damage in organelles, resulting in yield of viable blastocysts following in vitro embryo production.
|
|
| 40. |
- Aberg, D, et al.
(författare)
-
Implantation temperature dependent deep level defects in 4H-SiC
- 2001
-
Ingår i: Materials Science Forum, Vols. 353-356. ; , s. 443-446
-
Konferensbidrag (refereegranskat)abstract
- Deep level transient spectroscopy spectra of the near Z-defect region (150-350K) were investigated for B implanted samples of low doses (10(8)-10(9) cm(-2)). For 300 degreesC implantation, a level at an energy of 0.41 eV below the conduction hand edge was found, referred to as the S-level. The S-center was shown to form in both implanted and electron irradiated 4H-SiC, either after room temperature (R.T.) implantation followed by mild heat treatments or lung R.T. storage (several months) or after 200-300 degreesC implantations/irradiations. The S-center was found to anneal out at temperatures above 250 degreesC.
|
|
