A5020664307- Logic, programming, and type systems
- Parallel Computing and Optimization Techniques
- Distributed systems and fault tolerance
- Formal Methods in Verification
- Software Engineering Research
- Advanced Database Systems and Queries
- Software Testing and Debugging Techniques
- Real-Time Systems Scheduling
- Security and Verification in Computing
- Semantic Web and Ontologies
- Advanced Data Storage Technologies
- Distributed and Parallel Computing Systems
- Software Reliability and Analysis Research
- Model-Driven Software Engineering Techniques
- Optimization and Search Problems
- Data Management and Algorithms
- Simulation Techniques and Applications
- Algorithms and Data Compression
- Scientific Computing and Data Management
- Embedded Systems Design Techniques
- Data Quality and Management
- Petri Nets in System Modeling
- Software Engineering Techniques and Practices
- Software-Defined Networks and 5G
- Natural Language Processing Techniques
Victoria University of Wellington
2013-2022
University of Waikato
1980-1982
Despite years of research, the design efficient nonblocking algorithms remains difficult. A key reason is that current shared-memory multiprocessor architectures support only single-location synchronisation primitives such as compare-and-swap (CAS) and load-linked/store-conditional (LL/SC). Recently researchers have investigated utility double-compare-and-swap (DCAS)--a generalisation CAS supports atomic access to two memory locations -- in overcoming these problems. We summarise recent...
We describe an approach to verifying concurrent data structures based on simulation between two Input/Output Automata (IOAs), modelling the specification and implementation. explain how we used this in mechanically a simple lock-free stack implementation using forward simulation, briefly discuss our experience three other algorithms which all required use of backward simulation.
We describe an array-based nonblocking implementation of a concurrent bounded queue, due to Shann, Huang and Chen (2000), explain how we detected errors in the algorithm while attempting formal verification. first corrected errors, then modified obtain behaviour boundary cases. Both versions were verified using PVS theorem proven. verification algorithm, which subsumes proof version.
We describe ongoing work in which we aim to formally specify a correctness condition for transactional memory (TM) called Weakest Reasonable Condition (WRC), and facilitate fully formal machine-checked proofs that TM implementations satisfy the condition. To precisely define WRC condition, express it using an I/O automaton. similarly present another PRAG, is more restrictive, but closely reflects intuition about common implementation techniques. sketch simulation proof PRAG implements WRC,...
We develop a mechanized proof of Featherweight Java with Assignment and Immutability in the Coq assistant. This is step towards more machine-checked proofs non-trivial type system. used object immutability close to that IGJ [9]. describe challenges mechanisation encoding we inside Coq.
We report on the software development techniques used in New Zealand industry, paying particular attention to requirements gathering. surveyed a selection of companies with general questionnaire and then conducted in-depth interviews four companies. Our results show wide variety kinds undertaking development, employing range techniques. Although our data are not sufficiently detailed draw statistically significant conclusions, it appears that larger groups typically have more well-defined...
We show how a sophisticated, lock-free concurrent stack implementation can be derived from an abstract specification in series of verifiable steps. The algorithm is simplified version one described by Hendler, Shavit and Yerushalmi [Hendler, D., N. L. Yerushalmi, A scalable algorithm, in: SPAA 2004: Proceedings the Sixteenth Annual ACM Symposium on Parallel Algorithms, June 27–30, 2004, Barcelona, Spain, pp. 206–215], which allows push pop operations to paired off eliminated without...
Path dependent types have long served as an expressive component of the Scala programming language. They allow for modelling both bounded polymorphism and a degree nominal subtyping. Nominality in turn provides ability to capture first class modules. Thus single language feature gives rise rich array expressiveness. Recent work has proven path sound presence intersection recursive types, but unfortunately typing remains undecidable, posing problems programmers who rely on results type...
Correctness of concurrent objects is defined in terms conditions that determine allowable relationships between histories a object and those the corresponding sequential object. Numerous correctness have been proposed over years, more recently as algorithms implementing adapted to cope with multicore processors relaxed memory architectures. We present formal framework for defining architectures, covering both standard totally ordered newer memory, which allows them be expressed uniform...
Traditionally, formal semantic models of Java-like languages use an explicit model the store which mimics pointers and ram. These low level hamper understanding semantics, development proofs about ownerships other encapsulation properties, since real (graph) structure data is obscured by encoding. Such are also inadequate for didactic purposes they rely on run-time structures that do not exist in source program --- order to understand meaning expression middle execution one required...
It is well known that the principal operators in Z schema calculus are not monotonic with respect to refinement, which limits their usefulness software development. The usual reaction this observation remove all before performing any kind of or move a different formalism such as B refinement calculus. This paper examines interaction between and more closely, showing exactly how non-monotonicity arises, identifying various conditions under components expressions can be safely replaced by...