|
ROLE
 Author only
AUTHOR PROFILE PAGES (BETA)
Project background
BOOKMARK & SHARE
|
|
|
|
| Export results as:
BibTeX
EndNotes
ACM Ref
|
| 2009
|
1
|
|
A Graph-based Design Framework for Global Computing Systems
Antonio Bucchiarone, Greg Dennis, Stefania Gnesi
|
|
April 2009
|
|
Electronic Notes in Theoretical Computer Science (ENTCS)
, Volume 236
|
|
Publisher: Elsevier Science Publishers B. V.
|
|
| Bibliometrics: Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 0 |
 |
|
We present a framework for designing and analyzing Global Computing Systems using Dynamic Software Architectures. The framework, called TGG"A, integrates typed graph grammars and the Alloy modeling language to specify Programmed Dynamic Software Architectures ...
Keywords: Alloy, component-based software systems, dynamic software architectures, graph grammars
|
| |
|
| 2008
|
2
|
|
Bounded Verification of Voting Software
Greg Dennis, Kuat Yessenov, Daniel Jackson
|
|
October 2008
|
|
VSTTE '08: Proceedings of the 2nd international conference on Verified Software: Theories, Tools, Experiments
|
|
Publisher: Springer-Verlag
|
|
| Bibliometrics: Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 0 |
|
|
We present a case-study in which vote-tallying software is analyzed using a bounded verification technique, whereby all executions of a procedure are exhaustively examined within a finite space given by a bound on the size of the heap and the ...
|
| |
|
| 2006
|
3
|
|
Modular verification of code with SAT
Greg Dennis, Felix Sheng-Ho Chang, Daniel Jackson
|
|
July 2006
|
|
ISSTA '06: Proceedings of the 2006 international symposium on Software testing and analysis
|
|
Publisher: ACM
|
|
Full text available: |
 Pdf
(305.49 KB)
|
|
|
| Bibliometrics: Downloads (6 Weeks): 8, Downloads (12 Months): 42, Citation Count: 3 |
|
|
An approach is described for checking the methods of a class against a full specification. It shares with traditional model checking the idea of exhausting the entire space of executions within some finite bounds, and with traditional verification the ...
Keywords: SAT, alloy, first-order logic, formal methods, formal verification, software model checking
|
| |
|
| 2004
|
4
|
|
Automating commutativity analysis at the design level
Greg Dennis, Robert Seater, Derek Rayside, Daniel Jackson
|
|
July 2004
|
|
ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis
|
|
Publisher: ACM
|
|
Full text available: |
Pdf
(129.59 KB)
|
|
|
| Bibliometrics: Downloads (6 Weeks): 0, Downloads (12 Months): 23, Citation Count: 1 |
|
|
Two operations commute if executing them serially in either order results in the same change of state. In a system in which commands may be issued simultaneously by different users, lack of commutativity can result in unpredictable behaviour, even if ...
Keywords: OCL, alloy, case study, commutativity, concurrency, critical systems, formal specification, lightweight formal methods, model checking, proton therapy, radiation therapy, testing
|
Also published in: |
| July 2004 |
SIGSOFT Software Engineering Notes |
Volume 29 Issue 4 |
|
| |
|
| 1998
|
5
|
|
|
|
|
|
