https://bruda.ca/ 2026-05-24T19:25:27+00:00 https://bruda.ca/ https://bruda.ca/_media/wiki/dokuwiki.svg text/html 2026-04-30T15:17:44+00:00 stefan (stefan@undisclosed.example.com) https://bruda.ca/start <table><tr><th colspan="2" width="50%">Sat 3 Jan 2026 4:55 pm -0500</th><th colspan="2" width="50%">current</th></tr><tr><td class="diff-blockheader" colspan="2">Line 18:</td> <td class="diff-blockheader" colspan="2">Line 18:</td> </tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">====== Teaching ======</td><td class="diff-lineheader">&#160;</td><td class="diff-context">====== Teaching ======</td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context"></td><td class="diff-lineheader">&#160;</td><td class="diff-context"></td></tr> <tr><td class="diff-lineheader">-</td><td class="diff-deletedline"><strong class="diff-mark">This term (Winter 2026)&#160;</strong>I&#160;<strong class="diff-mark">teach [[http://cs</strong>.<strong class="diff-mark">ubishops.ca/home/cs310|CS 310 (Introduction to Software Specifications)]] and [[http://cs.ubishops.ca/home/cs464|CS 464/564 (Network Programming/Network Programming and Distributed Algorithms)]]</strong></td><td class="diff-lineheader">+</td><td class="diff-addedline">I&#160;<strong class="diff-mark">am not teaching over the summer</strong>.</td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context"></td><td class="diff-lineheader">&#160;</td><td class="diff-context"></td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">[[teaching|More...]]</td><td class="diff-lineheader">&#160;</td><td class="diff-context">[[teaching|More...]]</td></tr> </table> text/html 2026-01-03T21:53:17+00:00 stefan (stefan@undisclosed.example.com) https://bruda.ca/teaching <table><tr><th colspan="2" width="50%">Sat 3 Jan 2026 4:53 pm -0500</th><th colspan="2" width="50%">current</th></tr><tr><td class="diff-blockheader" colspan="2">Line 3:</td> <td class="diff-blockheader" colspan="2">Line 3:</td> </tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs310|CS 310, Introduction to Software Specifications]] (Winter 2026)</td><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs310|CS 310, Introduction to Software Specifications]] (Winter 2026)</td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs464|CS 464/564, Network Programming/Network Programming and Distributed Algorithms]] (Winter 2026)</td><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs464|CS 464/564, Network Programming/Network Programming and Distributed Algorithms]] (Winter 2026)</td></tr> <tr><td class="diff-lineheader">-</td><td class="diff-deletedline"></td><td colspan="2">&#160;</td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs317|CS 317, Design and Analysis of Algorithms]] (Fall 2025)</td><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs317|CS 317, Design and Analysis of Algorithms]] (Fall 2025)</td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs403|CS 403, Principles of Programming Languages]] (Fall 2025)</td><td class="diff-lineheader">&#160;</td><td class="diff-context">&#160; * [[http://cs.ubishops.ca/home/cs403|CS 403, Principles of Programming Languages]] (Fall 2025)</td></tr> </table> text/html 2025-07-26T12:50:51+00:00 stefan (stefan@undisclosed.example.com) https://bruda.ca/part/msc_theses <table><tr><th colspan="2" width="50%">Wed 2 Jul 2025 1:07 pm -0400</th><th colspan="2" width="50%">current</th></tr><tr><td class="diff-blockheader" colspan="2">Line 1:</td> <td class="diff-blockheader" colspan="2">Line 1:</td> </tr> <tr><td colspan="2">&#160;</td><td class="diff-lineheader">+</td><td class="diff-addedline">====== On the Equivalence between Must-Test Specifications and the Linear Temporal Logic ======</td></tr> <tr><td colspan="2">&#160;</td><td class="diff-lineheader">+</td><td class="diff-addedline">By Atefeh Farhadi, July 2025.&#160; Full paper: {{ :part:farhadi20250711.pdf |}}</td></tr> <tr><td colspan="2">&#160;</td><td class="diff-lineheader">+</td><td class="diff-addedline"></td></tr> <tr><td colspan="2">&#160;</td><td class="diff-lineheader">+</td><td class="diff-addedline">This paper explores the connections between two formal verification techniques: must testing and Linear Temporal Logic (LTL). Both are vital for validating system behaviors and ensuring proper operation. Must testing captures dynamic behaviors and ensures system requirements are met under all execution scenarios, while LTL specifies and verifies temporal properties within systems.&#160; Concretely, we explore the equivalence between must testing and LTL.&#160; We develop a practical (algorithmic) framework to translate must-test specifications into equivalent LTL formulas.&#160; While we thus go only half-way toward establishing an equivalence, we believe that the conversion the other way around is possible as well.&#160; On a practical note, we also note that model checking (the algorithmic LTL verification framework) is a very mature technology widely uses in practice, while must testing is deployed to a much lesser extent.&#160; We therefore argue that our conversion is much more useful for practical applications.&#160; This being said, a conversion of LTL formulae into equivalent must tests is a necessary future expansion of this study to establish formally the equivalence of the two frameworks.</td></tr> <tr><td colspan="2">&#160;</td><td class="diff-lineheader">+</td><td class="diff-addedline"></td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">====== On TorXakis Correctness as an ioco Implementation: An Empirical Model-Based Evaluation ======</td><td class="diff-lineheader">&#160;</td><td class="diff-context">====== On TorXakis Correctness as an ioco Implementation: An Empirical Model-Based Evaluation ======</td></tr> <tr><td class="diff-lineheader">&#160;</td><td class="diff-context">By Reza Ghasemi, May 2025.&#160; Full paper: {{ :part:ghasemi202505.pdf |}}</td><td class="diff-lineheader">&#160;</td><td class="diff-context">By Reza Ghasemi, May 2025.&#160; Full paper: {{ :part:ghasemi202505.pdf |}}</td></tr> </table> text/html 2025-07-26T12:49:49+00:00 stefan (stefan@undisclosed.example.com) https://bruda.ca/?image=part%3Afarhadi20250711.pdf&ns=part&do=media <table><tr><th width="50%"></th><th width="50%">current</th></tr><tr><td align="center"></td><td align="center"></td></tr></table> text/html 2025-07-02T17:05:27+00:00 stefan (stefan@undisclosed.example.com) https://bruda.ca/?image=part%3Aghasemi202505.pdf&ns=part&do=media <table><tr><th width="50%"></th><th width="50%">current</th></tr><tr><td align="center"></td><td align="center"></td></tr></table>