| 1. |
- Abad, Manuel David, et al.
(författare)
-
Identification of Ternary Phases in TiBC/a-C Nanocomposite Thin Films : Influence on the Electrical and Optical Properties
- 2011
-
Ingår i: Plasma Processes and Polymers. - : Wiley. - 1612-8850 .- 1612-8869. ; 8:7, s. 579-588
-
Tidskriftsartikel (refereegranskat)abstract
- The local structure of TiBC and amorphous carbon (a-C) nanocomposite films (TiBC/a-C) was correlated with their optical and electrical properties. TiBC/a-C films with increasing C content were deposited by magnetron co-sputtering from TiC:TiB(2) (60: 40) and graphite targets. Chemical composition is determined by electron energy-loss spectroscopy. Grazing incidence X-ray diffraction reveals that the microstructure of the films is amorphous with small nanocrystallites emerging by increasing the C content that could be attributed to the formation of ternary (TiB(x)C(y)) or mixed binary (TiB(2) and TiC) phases. Further information was then obtained by studying the chemical bonding by measuring the near-edge fine structure (NES) by electron energy-loss (B K-, C K-, and Ti L-edges) and X-ray absorption (B K-and Ti L-edges) spectroscopies. The NES analysis indicates the formation of a nanocrystalline ternary TiB(x)C(y) compound concomitant with the segregation of an a-C phase as the carbon content is increased. The optical properties were studied by spectroscopic ellipsometry and the electrical resistivity was measured by the Van der Pauw method between 20 and 300 K. The films continuously lose their metallic character in terms of optical constants and resistivity with increasing carbon content. Theoretical fitting of the electrical properties using the grain-boundary scattering model supported the formation of a nanocomposite structure based on a ternary TiB(x)C(y) phase embedded in a matrix of a-C. The electron transport properties are mainly limited by the high density of point defects, grain size, and transmission probability.
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
- 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
|
|
| 6. |
|
|
| 7. |
- 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.
|
|
| 8. |
- 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.
|
|
| 9. |
- 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.
|
|
| 10. |
- 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.
|
|
