Remove more unused pages that can also be found on the wiki

src/docs/chapter/other/Jens_Bendisposto_Conferences.adoc

-
-== Conferences
-
-* *VMCAI* International Conference on Verification, Model Checking,
-and Abstract Interpretation http://vmcai13.di.univr.it/Home.html
-* *CAV* International Conference on Computer Aided Verification
-http://cav12.cs.illinois.edu/cfp.html
-* *TCAS* International Conference on Tools and Algorithms for the
-Construction and of Analysis Systems http://www.etaps.org/2012/tacas
-http://www.etaps.org/2012/call-for-papers
-* *FMCAD* International Conference on Formal Methods in
-Computer-Aided Design http://www.cs.utexas.edu/users/hunt/FMCAD/
-* *FTSCS* International Workshop on Formal Techniques for
-Safety-Critical Systems
-http://www.ftscs.org/2012/index.php?n=Conference.CallForPapers
-* *ICST* International Conference on Software Testing,
-Verification, and Validation
-http://www.icst.lu/site/icst2013/call-for-papers
-* *INFINITY* International Workshop on Verification of Infinite-State
-Systems http://www.it.uu.se/workshop/infinity2012/
-* *DATE* Design Automation and Test in Europe
-http://www.date-conference.com/
-* *MoTiP* Workshop on Model-based Testing in Practice
-http://www.ourglocal.com/event/?eventid=19009
-* *ACES-MB* Workshop on Model Based Architecting and Construction
-of Embedded Systems
-http://www.artist-embedded.org/artist/Overview,2130.html
-* *SIGSOFT* International Symposium on the Foundations of Software
-Engineering http://sel.ifmo.ru/esec-fse2013/
-* *ISoLA* International Symposium on Leveraging Applications of
-Formal Methods, Verification, and Validation
-http://www.cs.uni-potsdam.de/isola/isola2012/pdf/isola-cfp2012.pdf
-* *ASE* International Conference on Automated Software Engineering
-http://ase2012.paluno.uni-due.de/calls/
-* *FASE* International Conference on Fundamental Approaches to
-Software Engineering http://www.etaps.org/2012/fase
-http://www.etaps.org/2012/call-for-papers
-* *PLDI* Conference on Programming Language Design and
-Implementation http://pldi12.cs.purdue.edu/content/calls-征稿启事
-* *ICSE* International Conference on Software Engineering
-http://2013.icse-conferences.org/submissions
-* *SAS* Static Analysis Symposium
-http://www.sas2012.ens.fr/#submission
-* *FM* International Symposium on Formal Methods
-http://www.fmeurope.org/?p=443
-* *SPIN* International SPIN Workshop on Model Checking of Software
-http://qav.cs.ox.ac.uk/spin2012/
-* *ATVA* International Symposium on Automated Technology for
-Verification and Analysis http://www.iarcs.org.in/atva2012/
-* *AVOCS* International Workshop on Automated Verification of
-Critical Systems http://www.swt-bamberg.de/AVoCS2012/callforpapers.php
-* *PDMC* International Workshop on Parallel and Distributed Methods
-in Verification http://www.pdmc.cz/PDMC12/
-* *BMC* International Workshop on Bounded Model Checking
-http://www.illc.uva.nl/LogicList/newsitem.php?id=1835
-* *MoChArt* Model Checking and Artificial Intelligence
-http://www.aaai.org/Workshops/ws13.php
-* *SBFM* Workshop on Systems Biology and Formal Methods
-http://cs.nyu.edu/~pcousot/SBFM2012/index.html
-* *MoCSeRS* Workshop on model checking secure and reliable systems
-http://www.comp.nus.edu.sg/~pat/MoCSeRS2010/submission.html
-* *ICFEM* International Conference on Formal Engineering Methods
-http://www.jaist.ac.jp/icfem2012/callforpapers/index.html
-* *DSN* International Conference on Dependable Systems and Networks
-http://2013.dsn.org/call-for-contributions/
-* *MBT* Model Based Testing, Satellite workshop of ETAPS European
-joint conference on Theory And Practice of Software
-http://mbt-workshop.org/
-* *SoftMC* Workshop on Software Model Checking
-http://www.cav2005.inf.ed.ac.uk/2005_call_for_papers.html

src/docs/chapter/other/Jens_Bendisposto_Model_Checkers.adoc

-
-== Model Checkers
-
-* *SPIN* http://spinroot.com/spin/whatispin.html
-* *PAT* http://www.comp.nus.edu.sg/~pat/
-* *MALPAS*
-http://www.atkinsglobal.co.uk/sectors-and-services/sectors/defence/documents/~/media/Files/A/Atkins-UK/Attachments/sectors/defence/library-docs/capability-statements/malpas.pdf
-* *Mocha* http://www.cis.upenn.edu/~mocha/
-* *Prism* http://www.prismmodelchecker.org/
-* *NuSMV* http://nusmv.fbk.eu/
-* *PVS* http://pvs.csl.sri.com/
-* *COMPASS* http://compass.informatik.rwth-aachen.de/about.html
-* *COSPAN*
-* *SMV* Symbolic Model Verifier
-http://www.cs.cmu.edu/~modelcheck/smv.html
-http://www.kenmcmil.com/smv.html
-* *NuSMV* http://nusmv.fbk.eu/
-* *Murphi* http://www.cs.utah.edu/formal_verification/Murphi/
-* *XMC* http://www.cav2005.inf.ed.ac.uk/2005_call_for_papers.html
-* *BLAST* http://mtc.epfl.ch/software-tools/blast/index-epfl.php
-* *DiVinE* http://divine.fi.muni.cz/
-* *Solibri* http://www.solibri.com/
-* *Bogor* http://bandera.projects.cis.ksu.edu/
-http://bogor.projects.cis.ksu.edu/
-* *MCK* http://cgi.cse.unsw.edu.au/~mck/pmck/
-* *YASM* http://www.cs.toronto.edu/~arie/yasm/
-* *SLAM* http://research.microsoft.com/en-us/projects/slam/
-
-Other Lists:
-
-* http://www.pst.informatik.uni-muenchen.de/~hammer/mc-list.html
-* http://en.wikipedia.org/wiki/List_of_Model_Checking_Tools

src/docs/chapter/reference/01_ABZ14.adoc

-[[abz14]]
-== ABZ 2014 Case Study
-
-This page provides additional resources for the journal article we have submitted for the
-http://sttt.cs.uni-dortmund.de/[International Journal on Software Tools for Technology Transfer].
-
-The journal article is an extended version of the paper we have submitted for the
-http://www.irit.fr/ABZ2014/casestudy.html[ABZ 2014 case study track].
-
-The full description of the case study can be found https://www3.hhu.de/stups/prob/images/d/df/Landing_system.pdf[here]
-
-[[prob-live-visualisations]]
-=== ProB Live Visualisations
-
-We have prepared two interactive live visualizations of the case study.
-One of our own Event-B model and one of the first development by
-Jean-Raymond Abrial and Wen Su footnote:[Aircraft Landing Gear System:
-Approaches with Event-B to the Modeling of an Industrial System, Su, W.
-and Abrial, J., 2014 in Communications in Computer and Information
-Science (ABZ 2014: The Landing Gear Case Study)].
-
-The visualization of our own model can either be controlled by
-interacting with the displayed elements (i.e., clicking the handle) or
-using the Events view which can be opened using the "Open View" menu
-at the bottom right corner. The other model can only be controlled using
-the Events view.
-
-http://wyvern.cs.uni-duesseldorf.de/bms/landing.html[Visualization of our own model]
-
-1.  http://wyvern.cs.uni-duesseldorf.de:18080/bms/vis_dev1_fixed/landinggear.html[Visualization
-of the model by Jean-Raymond Abrial and Wen Su (Temporally disabled)]
-
-[[bmotion-studio-for-prob-video]]
-=== BMotion Studio for ProB Video
-
-ifdef::basebackend-html[]
-++++
-<script>
-video::wFr_pEjbpqo[youtube]
-</script>
-++++
-endif::[]
-
-You can find the video https://youtu.be/wFr_pEjbpqo[here].
-
-
-=== Resources
-
-
-* https://www3.hhu.de/stups/downloads/pdf/abz14casestudy.pdf[ABZ 2014 Case Study Paper]
-
-* https://www3.hhu.de/stups/prob/images/7/77/LandingGear.zip[Landing Gear Model EventB Model]
-
-=== Links
-
-[[bmotion-studio-for-prob]]
-==== BMotion Studio for ProB
-
-
-* https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotion Studio
-for ProB Homepage]
-* https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotion Studio
-for ProB User Handbook]
-* https://github.com/ladenberger/bmotion-prob[BMotion Studio for ProB
-Sourcecode]
-
-[[prob-2.0]]
-==== ProB 2.0
-
-* https://github.com/bendisposto/prob2[ProB 2.0 Sourcecode]
-* https://www3.hhu.de/stups/downloads/[ProB 2.0 Downloadsite]
-* https://www3.hhu.de/stups/handbook/prob2/prob_tcltk.html[ProB 2.0 User Manual]

src/docs/chapter/reference/02_ABZ16.adoc

-[[abz16]]
-== ABZ 2016 Case Study
-
-[[the-hemodialysis-machine-case-study]]
-=== The Hemodialysis Machine Case Study
-
-This page provides additional information and resources for the paper we
-have submitted for the http://www.cdcc.faw.jku.at/ABZ2016[ABZ 2016 case study track].
-
-The full description of the case study can be found http://www.cdcc.faw.jku.at/ABZ2016/HD-CaseStudy.pdf[here].
-
-==== Resources
-
-* http://www.cdcc.faw.jku.at/ABZ2016/HD-CaseStudy.pdf[ABZ 2016 Case Study Paper]
-
-The original specification of the HD machine as PDF.
-
-* https://www3.hhu.de/stups/prob/images/d/d3/HDMachine-160122.zip[HD Machine Event-B Model]
-
-The zip file contains the HD machine Event-B model. You can import the
-zip file directly into the Rodin platform as an Event-B project.
-
-* https://www3.hhu.de/stups/prob/images/b/bf/Cosim-160122.zip[Co-Simulation Model of the Blood Flow Control]
-
-The zip file of the co-simulation model contains a readme file that
-explains what is included.
-
-* https://www3.hhu.de/stups/prob/images/3/39/HDMachine-BMS-160122.zip[BMotion Studio Visualisation]
-
-The zip file contains the domain specific visualisation of the HD
-machine developed with BMotion Studio. You need to
-https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[download]
-the latest version of BMotion Studio (v.0.2.7). Some instruction for
-getting started with BMotion Studio can be find
-http://www3.hhu.de/stups/handbook/bmotion/current/html/first_steps.html[here].
-
-[[live-visualisation]]
-==== Live Visualisation
-
-* http://wyvern.cs.uni-duesseldorf.de/bms/hdmachine.html[BMotion Studio
-Visualisation of the HD Machine]
-
-If you have problems in running the visualisation, please contact Lukas
-Ladenberger (ladenberger@cs.uni-duesseldorf.de)
-
-==== Links
-
-* https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotion Studio for ProB Homepage]
-* https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotion Studio for ProB User Handbook]
-* http://wiki.event-b.org/index.php/IUML-B[iUML-B Homepage]
-* https://www3.hhu.de/stups/handbook/rodin/[Rodin Handbook]

src/docs/chapter/reference/03_FormalPrototyping.adoc

-[[formal_prototyping]]
-== Formal Prototyping
-
-This page provides additional information and resources for the tool paper
-we have submitted for the http://staf2016.conf.tuwien.ac.at/sefm/[SEFM 2016 conference].
-
-=== Resources
-
-* https://www3.hhu.de/stups/prob/index.php/BMotionWeb_Download[BMotionWeb Download]
-* https://www3.hhu.de/stups/prob/images/d/de/Phonebook.Formal.Prototype.zip[Phonebook Formal Prototype]
-* https://www3.hhu.de/stups/prob/images/1/1a/CCS.Formal.Prototype.zip[Cruise Control System Formal Prototype]
-
-[[live-online-formal-prototypes]]
-=== Live Online Formal Prototypes
-
-* http://wyvern.cs.uni-duesseldorf.de/bms/phonebook.html[Phonebook Online-Version]
-* http://wyvern.cs.uni-duesseldorf.de/bms/ccs.html[Cruise Control System Online-Version]
-
-Please note, that the visual editor is only available in the
-desktop-version of BMotionWeb.
-
-If you have troubles with running the online version, please contact
-Lukas Ladenberger (ladenberger@cs.uni-duesseldorf.de).
-
-=== Links
-
-* https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotionWeb Homepage]
-* https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotionWeb User Handbook]
-
-[[getting-started-with-bmotionweb]]
-=== Getting Started with BMotionWeb
-
-WARNING: BMotionWeb is currently not up-to-date and not in use anymore. BMotion Studio however can still be downloaded with our ProB Plugin for Rodin.
-
-[[install-bmotionweb]]
-==== Install BMotionWeb
-
-Start off by downloading BMotionWeb for your operating system.
-Decompress the archive and expand the directory if necessary. Navigate
-to the application folder and start BMotionWeb by executing the
-bmotion-prob binary.
-
-[[open-a-formal-prototype]]
-==== Open a Formal Prototype
-
-Start off by downloading a formal prototype from this wiki page.
-Decompress the archive and expand the directory if necessary. To open a
-formal prototype, click on the box in the middle of the window and
-select the BMotionWeb manifest file (.json file) of the formal prototype
-or just drag and drop the manifest file into the box. You can also open
-a formal prototype via the top menu: File > Open Visualization. For
-instance, to load the phonebook or CCS formal prototype select the
-phonebook.json or ccs.json file respectively.

src/docs/chapter/reference/04_ProjectionDiagram.adoc

-[[projection-diagram]]
-== Mastering the Visualization of Larger State Spaces with Projection Diagrams
-
-NOTE: This page provides additional resources for the paper for http://icfem2015.lri.fr/[ICFEM 2015].
-
-[[resources-and-prob-live-visualizations]]
-=== Resources and ProB Live Visualizations
-
-We have prepared two interactive live visualizations. One of the Event-B
-model of the landing gear system (the full description of the case study
-can be found https://www3.hhu.de/stups/prob/images/d/df/Landing_system.pdf[here]) and one of the Event-B
-model of a simple lift system.
-
-The visualizations can either be controlled by interacting with the
-displayed elements (i.e., clicking the handle) or using the Events view
-which can be opened using the "Open View" menu at the bottom right
-corner.
-
-1.  http://wyvern.cs.uni-duesseldorf.de/bms/landing.html[Visualization
-of the landing gear system]
-2.  http://wyvern.cs.uni-duesseldorf.de/bms/lift.html[Visualization of
-the simple lift]
-
-The Event-B model of the simple lift system be can be downloaded https://www3.hhu.de/stups/prob/index.php/File:SimpleLift.zip[here].
-
-http://stups.hhu.de/w/Special:Publication/LadenbergerLeuschel_ProjectDiagram[Technical
-Report]
-
-[[creating-a-domain-specific-projection]]
-==== Creating a Domain Specific Projection
-
-* Open the ModelCheckingUI using the "Open View" menu at the bottom
-right corner.
-* Click on the "MC" icon and run the model checker in order to explore
-the full state space of the model.
-* After finishing, you can open the Element Projection view using the
-"Open Diagram" menu at the bottom right corner.
-* Select the lift or landing visualization respectively and select some
-elements for the projection.
-
-Please note: Due to a small bug, you can only create a projection for
-max. two selected graphical elements at the moment. We are already
-working on this bug.

src/docs/chapter/reference/05_Sefm2015.adoc

-[[sefm2015]]
-== Benchmarks for the ProB (Dis)prover
-
-We benchmarked the ProB disprover for an article for SEFM 2015.
-
-=== Raw Data
-
-All raw data is available as csv files from
-https://www3.hhu.de/stups/models/sefm2015_disprover/raw/[here].
-A zip file containing all csv files is available
-https://www3.hhu.de/stups/models/sefm2015_disprover/raw/rawdata.zip[here].
-
-=== Data Visualisations
-
-Due to the page limit, we could not give all the diagrams and
-visualisation of the benchmark results in the article. They are
-available here:
-
-==== Landing Gears
-
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial1_provers_only.pdf[Su
-and Abrial, Landing Gear Model 1, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial1_tactic.pdf[Su
-and Abrial, Landing Gear Model 1, Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial2_provers_only.pdf[Su
-and Abrial, Landing Gear Model 2, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial2_tactic.pdf[Su
-and Abrial, Landing Gear Model 2, Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial3_provers_only.pdf[Su
-and Abrial, Landing Gear Model 3, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial3_tactic.pdf[Su
-and Abrial, Landing Gear Model 3, Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/landinggearfinal_provers_only.pdf[Hansen
-et. al., Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/landinggearfinal_tactic.pdf[Hansen
-et. al., Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/mammarlaleau_provers_only.pdf[Mammar
-and Laleau, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/mammarlaleau_tactic.pdf[Mammar
-and Laleau, Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/nantes_provers_only.pdf[André,
-Attiogbé and Lanoix, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/nantes_tactic.pdf[André,
-Attiogbé and Lanoix, Tactics]
-
-==== Further Models
-
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/canbus_provers_only.pdf[Colley,
-Canbus, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/canbus_tactic.pdf[Colley,
-Canbus, Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_provers_only.pdf[Andriamiarina
-and Méry, Graphcoloring, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_tactic.pdf[Andriamiarina
-and Méry, Graphcoloring, Tactics]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_provers_only.pdf[Wiegard,
-Stuttgart 21, Provers alone]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_tactic.pdf[Wiegard,
-Stuttgart 21, Tactics]
-
-==== Summaries
-
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/tactic_landiggears.pdf[Tactics
-on Landing Gears]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/tactic_all_models.pdf[Tactics
-on all Models]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/provers_alone_landiggears.pdf[Provers
-alone on Landing Gears]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/provers_alone_all_models.pdf[Provers
-alone on all Models]
-
-==== Surplus of ProB
-
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/surplus.pdf[Surplus
-of ProB (added last)]
-* https://www3.hhu.de/stups/models/sefm2015_disprover/output/surplus2.pdf[Surplus
-of ProB (added first)]