Sciweavers

WADT
2001
Springer
14 years 11 days ago
Verifying a Simple Pipelined Microprocessor Using Maude
Abstract. We consider the verification of a simple pipelined microprocessor in Maude, by implementing an equational theoretical model of systems. Maude is an equationally-based la...
Neal A. Harman
TACS
2001
Springer
14 years 11 days ago
Strong Normalization of Second Order Symmetric Lambda-mu Calculus
Parigot suggested symmetric structural reduction rules for ion to µ-abstraction in [9] to ensure unique representation of data type. We prove strong normalization of second order ...
Yoriyuki Yamagata
TACS
2001
Springer
14 years 11 days ago
Lightweight Analysis of Object Interactions
The state of the practice in object-oriented software development has moved beyond reuse of code to reuse of conceptual structures such as design patterns. This paper draws attenti...
Daniel Jackson, Alan Fekete
TACS
2001
Springer
14 years 11 days ago
A Logic Programming Language Based on Binding Algebras
We give a logic programming language based on Fiore, Plotkin and Turi’s binding algebras. In this language, we can use not only first-order terms but also terms involving variab...
Makoto Hamana
TACS
2001
Springer
14 years 11 days ago
The UDP Calculus: Rigorous Semantics for Real Networking
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the c...
Andrei Serjantov, Peter Sewell, Keith Wansbrough
TACS
2001
Springer
14 years 11 days ago
Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems
Lossy channel systems are systems of finite state automata that communicate via unreliable unbounded fifo channels. Today the main open question in the theory of lossy channel sy...
Ph. Schnoebelen
TACS
2001
Springer
14 years 11 days ago
Model-Checking LTL with Regular Valuations for Pushdown Systems
Javier Esparza, Antonín Kucera, Stefan Schw...