Switcher Labs SA | Yverdon-les-Bains, Switzerland | fully or partially REMOTE

Position: Senior Software Engineer

Domain: Video Graphics Engine | GPU

We develop a video graphics engine in C/OpenGL and Swift/Metal capable of transforming video feeds, projecting video on 3D surfaces and combining video with animated elements like textes, shapes or images. This rendering engine can work with live video feeds in real time or can be used to compose recorded video off-screen. It’s the main element of the Switcher Studio app.

We are looking for a Senior Software Engineer able to:

- Understand the mathematics and the software technologies needed to implement additional visual effects.

- Architect and organize complex code, design modules with clear APIs.

If you don’t know Metal, OpenGL or Swift but love mathematics, graphics and well structured software, please apply.

For working on site as an employee, you must be legally authorized to work in Switzerland or be an EU citizen. For working remotely as an employee or as a contractor you must be located in CH, EU or US.

Please apply by email: jobs-ch@switcherstudio.com

I have written one here: http://loup-vaillant.fr/tutorials/fast-scalarmult

It explains various constant time and variable times ways to do scalar multiplication (assuming constant time point addition), and clearly marks what is constant time (like combs) and what is variable time (like sliding windows).

One big missing part is modular multiplication, needed to perform constant time point addition. I explain some of it in my Poly1305 tutorial (search for "Cheating at modular arithmetic"): http://loup-vaillant.fr/tutorials/poly1305-design

My research group (I'm a PhD student) is working on algorithms that learn logic programs from examples and background knowledge (also given as logic programs). The programs our algorithms learn are first order definite datalog programs, which means they are sets of first order Horn clauses without negation as failure and without any functions of arity more than 1 as arguments of literals or terms.

The reason for the restriction is completeness and efficiency. Definite datalog programs are guaranteed to terminate (given a finite predicate and constant signature), so the search for a hypothesis (the learned program) cannot "go infinite" even when the target theory (what you are trying to learn) is recursive, even when it has mutually recursive clauses. As a result our algorithms can learn recursive programs (which, is rather important). The space of hypotheses doubles in size when negation as failure is allowed, which improves the efficiency of the search for hypotheses.

The problem of course is that some programs cannot be expressed in definite datalog than can be expressed in Prolog with negation as failure and arbitrary functions as arguments. So that's a bit of a limitation. For instance, one has to jump through hoops to learn programs with "exceptions" (A if B except if C), say like a program calculating leap years (which have exceptions for years divisible by 100 and 400) or fizzbuzz.

This is not directly programming with datalog- it's machine learning of datalog programs from data. But I think it's similar to the experience you're asking for.

My group's algorithms:

Metagol (a meta-interpretive learner for definite datalog programs):

https://github.com/metagol/metagol

Louise (a polynomial-time version of Metagol):

https://github.com/stassa/louise

   Our algorithm ...

Unless I completely misunderstand what you write, the approach you describe is the standard way of setting up SMT-solvers by interaction between a SAT solver with a theory solver. I think it is called lazy SMT or DPLL(T) in [1] where this approach seems to have been described first. [2] is also an interesting description of the phenomenon.

[1] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, C. Tinelli, DPLL(T): Fast Decision Procedures. https://www.cs.upc.edu/~oliveras/espai/papers/dpllt.pdf

[1] R. Nieuwenhuis, A. Oliveras, C. Tinelli, Abstract DPLL and Abstract DPLL Modulo Theories. http://www.cs.upc.edu/~roberto/papers/lpar04.pdf

For uBlock Origin users, you can inject this style by going go the UBO dashboard, navigating to the "My Filters" tab, and adding this line:

   github.com##relative-time::before:style(content: attr(title); margin-right: 0.5em;)

then hitting "Apply changes".

I think this is going to be well outside the pricing range for most people to use for an extended period of time, which is necessary for learning a lot. Depends on the specs of the developer AMI, too, which comes with Vivado and everything. But synthesis can be insanely CPU intensive for large designs, so who knows how they'll spec it. It might cost more due to including a Vivado license. And you'll need to do extensive amounts of testing, no matter what you're doing, so be prepared to synthesize and test on "Real World" F1 instances, on top of simulating, testing, etc.

If you truly want to get started with FPGAs, you can do it on a small chip, with an open source Verilog toolchain, and open source place/route/upload. Textual source code -> hardware upload, open source. Today, for like $50! I think this is way better as a tool for educational purposes, and a lot cheaper. Also, you don't have to deal with a giant bundle of EDA crapware.

What you want is Project IceStorm, the open source Verilog flow for iCE40 FPGAs: http://www.clifford.at/icestorm/ -- you install 3 tools (Yosys, Arachne P&R, IceStorm) and you're ready to go. It's all open source, works well, and the code is all really good, too.

You can get an iCE40 HX8k breakout board for $42, and it has ~8,000 LUTs. Sure, it's small, but fully open source can't be beaten and that's cheap for learning: http://www.latticestore.com/products/tabid/417/categoryid/59...

I think this is a much better route for learning how to program FPGAs, personally, with high quality software and cheap hardware -- just supplement it with some Verilog/VHDL books or so. There are pretty decent Verilog tutorials on places like https://www.nandland.com or https://embeddedmicro.com/tutorials/beginning-electronics for example.