Project Seminar "Formal Methods II" (326.090, SS 2010)
Abschnittsübersicht
-
Project Seminar "Formal Methods II" (326.090, SS 2010)
Time: Wednesday, 12:30-14:00
Place: Hagenberg Seminar Room
Start: March 10, 2010
In this seminar, we explore current research and systems for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...). This continues the seminar of the previous semester.
To take part in the seminar, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum. -
March 10
- Discussion of organization and seminar topics
-
March 24
- Wolfgang Schreiner: The RISC Program Explorer (First status report)
- Report on the current status of the RISC ProgramExplorer.
-
- Discussion on Article
David Parnas: Really Rethinking 'Formal Methods'
IEEE Computer: January 2010 (Vol. 43, No. 1) pp. 28-34
-
- Discussion on Article
David Parnas: Really Rethinking 'Formal Methods'
IEEE Computer: January 2010 (Vol. 43, No. 1) pp. 28-34 -
May 26
- George Rahonis,
Quantitative logicsWe present a quantitative MSO-logic for finite and infinite words over semirings. Weighted MSO-formulas are represented as formal power series. For this, we require our semirings to satisfy concrete completeness axioms. The semantics of sentences from a fragment of this logic coincide with the behaviors of weighted automata. If the underlying semiring is the max-plus semiring, then we consider for our logic discounting parameters, so that infinite sums exist. Next, we deal with quantitative LTL with discounting. Again weighted LTL-formulas are represented as formal power series over infinite words. Every weighted LTL-formula with a restricted syntax is expressively equivalent to a weighted automaton. We conclude by addressing a list of open problems connected to potential practical applications. - George Rahonis,
-
- Discussion on Article
David Parnas: Really Rethinking 'Formal Methods'
IEEE Computer: January 2010 (Vol. 43, No. 1) pp. 28-34 -
- Gabor Guta: Automatic Refinement of Model Transformations by Examples
- Gabor Guta: Automatic Refinement of Model Transformations by Examples
-
- Tamas Berczes, University of Debrecen
AddOn development for SAP Business One
The Sap Business One (SBO) is an integrated ERP software that targets business software requirements of small and medium sized companies. During the software implementation, many times have to modify the business logic or have to make vertical or horizontal AddOn-s to manage the entire processes of companies. Integration can be achieved using SAP Business One Software Development Kit (SDK). In this presentation we describe our powerful software framework, which is good for fast development integrated SBO AddOn, and for making independent software too. Softwares developed with our framework could be running integrated to SBO and could be running independently. -
-
Dr. Safeeullah Soomro, Yanbu University College, Saudi Arabia
How Static Analysis of Programs Helps to Locate and Localize Bugs Using Specification Knowledge
Locating faults is one of the most time consuming task in today's fast paced economy. Testing and formal verification techniques like model-checking are usually used for detecting faults but do not attempt to locate the root-cause for the detected faulty behavior. This presentation makes use of an abstract dependencies between program variables for detecting and locating faults in alias-free programs in cases where an abstract specification is available. In particular we show that the dependence model is correct. Whenever the dependence model reveals a fault there is a test case, which also reveals a fault.
I defended PhD in 2007 from Graz University of Technology, Austria. I have been carrying research at Graz University of Technology, Austria since 2003 to 2007. I have been involved in research and teaching since 1998. I have been teaching in different institutes in Pakistan. My main research areas are focused around software debugging, formal verification and software testing. In particular I am interested in applying model-based diagnosis and reasoning techniques to the field of automated software debugging of Java programs. Furthermore I am interested to carry research in the formal methods. I have been an author of several national and international publications in different reputed conferences, Books and journals. I am a reviewer and committee member of different international and national conferences. I have more than 10 years of experience of teaching and research. I am an approved supervisor by Higher Education Commission (HEC) Pakistan and can supervise PhD Students. I am a member of IEEE, IEEE Computer Society and SUCSA. Previously I supervised MS students from top ranked University NU-FAST) at Pakistan. I am an editor of three Book which is published by INTECHWEB which is an European organization.
-