Bergen Language Design Laboratory (BLDL)
BLDL has an internal meeting series. Some of these have a content which may be of interest to a larger audience. The program of these are announced here.
Contact Magne Haveraaen for more information.
Seminars 2016
- Domain Engineering week Monday 2016-11-07 through Friday 2016-11-11, every day 1015-1600
Dines Bjørner (Dept. of Mathematics and Computer Science, Technical University of Denmark):
The Triptych of Software Engineering - A Comprehensive ApproachMonday
2016-11-07Dines Bjørner: Manifest domains I 10-16 Room B, VilVite Tuesday
2016-11-08Dines Bjørner: Manifest domains II 10-12 Room B, VilVite
12-16 Room 4, VilViteWednesday
2016-11-09Doreen Tuheirwe (Dept. of Computer Science, Makerere University, Uganda): Domain engineering for weather information services
Dines Bjørner: The triptych approach III10-12 Room B, VilVite
12-16 Room 4, VilViteThursday
2016-11-10Kjetil Kjørstad, Roar Mjelde, Sveinung Rundhovde, Eirik Suther (INF220 student team): Domain engineering the Sphero robot
Dines Bjørner: The triptych approach IV10-16 Room C, VilVite Friday
2016-11-11Magne Haveraaen: Domain engineering the Magnolia way
Dines Bjørner: The triptych approach V10-16 Room C, VilVite The course is on the first two phases of the triptych software development method of (1) domain and (2) requirements engineering methods -- emphasising such that relate these in mathematical as well as technical ways: (a) a calculus of domain analysis & description prompts; (b.1) intrinsic, support technology, management & organisation, rules & regulation, and human behaviour facets of domains; and (b.2) projection, instantiation, extension and initialisation of domain requirements.
More course details and general background
The course is based on Dines Bjørner's recent paper "Manifest domains: analysis and description". Form Asp Comp (2016), doi:10.1007/s00165-016-0385-z.Bio
Professor Dines Bjørner (born 1937) is a Danish computer scientist. He specializes in research into domain engineering, requirements engineering and formal methods. Bjørner has been central to the formal methods and software development communities since the start of his carrier in 1962 at IBM laboratories. He was responsible for establishing the United Nations University Institute for Software Technology (UNU-IIST), Macau, in 1992, and was its first director. In 1985 Bjørner became a knight of the Order of the Dannebrog. From 1976 until his retirement in 2007 he was a professor at the Technical University of Denmark (DTU), and he is still active in the research community. - Thursday 2016-10-20 1415-1500,
Store auditorium, Høyteknologisenteret.
Albert Rubio (Departament de Ciències de la Computació, Universitat Politècnica de Catalunya), Barcelona, ES):
Scalable Program Analysis Techniques using Max-SMT
(slides)Program analyis is a formal method in which properties of computer programs are proved mathematically. As such it complements testing of programs, which cannot guarantee the absence of errors. The foundations of program analysis have been laid by Turing, Floyd, Dijkstra and Hoare in the 1950s and 60s. The method was long considered impracticable for real-life programs, but this has changed in recent years. Breakthroughs in SAT-solving have paved the way for (largely) automatic program analysis. In this talk we will provide an overview of the Max-SMT solving techniques and its application to compositional program analysis. These techniques have successfully been implemented in the VeryMax tool which currently can check safety, reachability and termination properties of C++ code.
Bio
Albert Rubio is Full Professor at the Technical University of Catalonia - BarcelonaTech, Spain. He started his research on automated deduction and (higher-order) rewriting. He has also worked in the development of SMT solvers within the Barcelogic team and recently he has started a new line of research on the application of Max-SMT solvers in program analysis. Albert is Chair of the Steering Committee of the International Termination Competition, has been invited speaker at RTA and LOPSTR, and has been PC member in many international conferences (LICS, CADE, IJCAR, FOSSACS, CSL, LPAR, RTA, etc.). - Wednesday 2016-10-19 1415-1500,
Room 405O2, Høyteknologisenteret.
Albert Rubio (Departament de Ciències de la Computació, Universitat Politècnica de Catalunya), Barcelona, ES):
Proving termination through conditional termination
(slides) - Wednesday 2016-06-15 1415-1600,
Lille auditorium, Høyteknologisenteret.
Zhiming Liu (Centre for Research and Innovation in Software Engineering (RISE), Faculty of Computer Science and Information Science, Southwest university, Chongqing, China):
Formal Model-Driven Design of Evolving Component-Based SystemsWith these two talks, we reflect on the development of the rCOS method for model-driven design of object and component software. Instead of going into technical details, the discussion will focus on what it is, the main ideas behind it, and where it is heading. We especially look into the possibility of extending the rCOS to modelling, design and maintain the so called Cyber-Physical Systems (CPS). For this, we discuss about a few points of understanding about CPS. We take a rather general view that a CPS is a network of digital computing components (or cyber components) and physical components interacting through interfaces. A cyber component senses its environment through interfaces, processes the information, and makes control decisions to control physical components through interfaces, and/or provide services to its users. Physical components may directly interact too, interfering or disturbing each other through physical interfaces. With the perspective that a CPS has an ever evolving architecture, we see an essential aspect of CPS development is to based on existing CPS as infrastructure design further cyber-physical components and integrate them into the system. We thus propose the need of an interface-based model for model-driven design of CPS components.
Bio
Zhiming Liu is known for his work on fault-tolerant program design and verification by transformations that established a theory of fault-tolerant refinement, and his work on the rCOS method. He joined Southwest University in Chongqing (China) as a professor in January 2016, and he is now leading to build the Centre for Research and Innovation in Software Engineering. Zhiming Liu received his PhD in 1991 from the University of Warwick (UK), and then worked there for three more years as a postdoc research fellow till 1994. After that, he worked during 1994-2005 at the University of Leicester as lecturer. Between 2002 and 2013, he worked for the United National University – International Institute for Software Technology (UNU-IIST, Macau) as a research fellow and then senior research fellow. Then he worked from 2013 to 2015 at Birmingham City University as Professor of Software Engineering before he returned back China to take his current position. The key bibliographic database lists over 150 of his peer reviewed publications in recognized outlets. These include papers published in the top journals on formal methods, ACM Transactions on Programming Languages, Formal Aspects of Computing, Science of Computer Programming and Theoretical Computer Science. - Monday 2016-06-13 1415-1500,
Lille auditorium, Høyteknologisenteret.
Arnaud Gotlieb (The Certus Centre, Simula, Oslo, Norway)
An overview of Constraint-Based TestingThese last years have seen the development of several constraint solving techniques dedicated to the testing of software systems, in an area called ``Constraint-Based Testing''. Our approach in this domain consists in exploring how Constraint Programming techniques can help the automatic generation of test cases for imperative programs. My talk will review different techniques including dynamic symbolic execution, path-based exploration and constraint-based exploration and will emphasize the developments of tools for C and Java programs.
Bio
Arnaud Gotlieb is a French research scientist in Computer Science, currently leader of the Certus Centre, Simula’s Centre for Research-based Innovation (SFI) on Software Verification & Validation. Dr. Gotlieb’s expertise is on the application of constraint solving to software testing. At the beginning of his career, he spent 7 years in Industry working for Dassault Electronics, Thomson-CSF and Thales. He joint INRIA, the French National Institute on Computer Science and Automatisms in 2002 where he made advances on constraint-based testing in a group specialized in static analysis and verification. He has contributed to several projects that aimed at improving static analysis, testing and verification tools of critical embedded software in civil and military avionics. He was the coordinator of the ANR CAVERN project (2008-2011) that explored the capabilities of constraint programming for program verification and participated to several large European Project proposals. Since October 2011, he has joint the Simula Research Lab. in Norway, as a senior research scientist. He is the main author of more than forty publications and co-author of more than seventy, and he is the main architect of several constraint-based testing tools for the testing of C and Java programs. He has served in the program committee the IEEE International Conference on Software Testing, Validation and Verification (ICST) since 2008 and many other conferences such as ISSRE, TAP, CP, SEIP, he co-chaired the technical program of QSIC in 2013 and the SEIP track of ICSE in 2014 and he will co-chair the Testing and Verification track of CP in 2016. He initiated the Constraints in Software Testing, Verification and Analysis (CSTVA) workshop series and was its main organizer during the first editions. He successfully co-supervised ten PhD students and was the head of the Software Engineering department at Simula from 2012 until 2015. He completed his PhD on automatic test data generation using constraint logic programming techniques in 2000 at the University of Nice-Sophia Antipolis and got habilitated (HDR) in Dec. 2011 from University of Rennes, France. - Tuesday 2016-05-31 1415-1500,
Lille auditorium, Høyteknologisenteret.
Mikhail Barash (Turku Centre for Computer Science, Turku, Finland)
Grammars for programming languagesContext-free grammars have been a model for defining syntax of various kinds of languages since the early days of computer science and they found their foremost application in specifying programming languages. However, their expressive power turned out to be insufficient to express many useful constructs, such as cross-reference, which reduces their applicability.
The present work attempts to implement N. Chomsky’s idea (1959) of a phrase-structure rule applicable in a context and introduces an extension of context-free grammars equipped with operators for referring to left and right contexts of the substring being defined. In this model, a rule, for example, A → a & ◃ B & ▹ C defines a symbol a, as long as it is preceded by a string defined by B and followed by a string defined by C. The conjunction operator in this example is taken from conjunctive grammars (A. Okhotin, Conjunctive grammars, J. Autom., Lang. Comb., 2001), which are an extension of ordinary context-free grammars that maintains most of their practical properties, including many parsing algorithms.
The present work gives two equivalent definitions of the new model of grammars with contexts: by logical deduction and by language equations, and establishes some basic properties of the model, including a cubic-time general parsing algorithm; this time can be improved to linear for LL and LR-subclasses of grammars. A variety of examples of grammars with contexts is constructed, with the most extensive example completely specifying the syntax of a simple typed programming language.
Short bio:
Mikhail Barash is a researcher and scientific coordinator in Turku Centre for Computer Science (Turku, Finland). His research interests include formal grammars, parsing algorithms, and compiler construction and implementation. Mikhail obtained his Ph.D. degree in Discrete Mathematics from University of Turku, Finland, focusing on studying different extensions of context-free grammars and their applications to defining syntax of programming languages.
VilVite auditorium is in VilVite, Thormøhlensgt 51.
Conference room D is in VilVite, Thormøhlensgt 51.
Lille auditorium is in Datablokken, Høyteknologisenteret, Thormøhlensgt 55.
Stort auditorium is in Datablokken, Høyteknologisenteret, Thormøhlensgt 55.